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;