4.10 Introduction of New Variable(Set, reconsider)
When we introduce a new variable, we write as follows.
set r1 = r + 2;
Therefor we can introduce the new variable r1 as (r + 2). The type will
turn into real number type, if r is real number type. In the bloc after
this sentence, we can use a variable r1 freely (if it escapes from the
bloc by end, r1 will become null and void). When we want to introduce the
new variable from which a type differs, we use reconsider. we write as
follows.
reconsider n1 = r + 2 as Nat by A2;
In this case, it is needed to attach a reason that r+2 becomes a natural
number type. It is same in Set that the new variable is effective only
in the bloc. We can also introduce two or more variables simultaneously
like the following.
reconsider n1 = r + 2, n2 =r + 3 as
Nat;