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 (a kind of computer language) and there is set for a general mode. Other than this, there are Nat, 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 Natin Real and Real in set. Functor and others are subordinated to mode. This is similar to a programming language. And it is considered that Any and set are the same.

    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 Function;
     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 Function. 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 Function. 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 Function as well as Real.