Mizar/mode型
表示
< Mizar
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,...} |