Mizar/mode型

mode 型

Any = set	Element 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,...}