コンテンツにスキップ

Mizar/mode型

出典: フリー教科書『ウィキブックス(Wikibooks)』

mode 型

Any = setElement of COMPLEX Real Integer Nat
 ...
   
   
Function    
   
Top Space   
   
 ...   
   

型の宣言方法

reserve X for 型;

型変換

reserve X for 型;
...
reconsider Y=X as 型 by 定義ファイル:番号;


例 : 複素数 X を Y に変換する
reserve X for Element of COMPLEX;
...
reconsider Y=X as complex number by XCMPLX_0:def 2;
mode cluster
複素数 Element of Complex complex number∀a,b∈実数,i=虚数 a + bi
実数 Real real number -∞ < Real < ∞
自然数 NAT natural number {0,1,2,...}