Chapter 5

About Mode

5.1 Mode

Next, we will explain mode. In Mizar, there is a concept of mode. Mode is a type of Pascal and there is Any for a general mode. Other than this, there are set, Real, and others as representative modes. Users can also define a mode. Also, as shown in the following figure, mode has a structure level such as Nat in \verb| Real| and \verb| Real| in Any. Functor and others are subordinated to mode. This is similar to a programming language.

For example, let us think about the following example. Here, let us assume that + is only defined pertaining to Real.



  reserve A,B for Real;



          C,D for Nat;



  L:C=A+B;



    ......



    D=A by...;



    then C=D+B by L;

Let us assume that C=A+B and D=A are demonstrated when A,B is Real and C is Nat. At this point, if we substitute D=A to a formula C=A+B and make C=D+B by L, it will be an error. It is because D and B have different modes. A calculation unit + is only defined to Real and it is not defined to Nat. Therefore, an error of unknown functor will appear.

This error can be taken care of by extending the mode of variable D. It will be fine if we can state that D is Nat as well as Real.