Mizar/定義型
< Mizar
Mizarの定義型 | 意味 | 使用法 | 必要な証明 | |
func | functor | 機能を持たせるもの | 演算子など | existence,uniqueness |
cluster | 群、まとまり | 新しいデータタイプを作成 | existence | |
mode | 型 | existence | ||
pred | predicate | 述語 | 因子、要素 | |
defpred | (definition)+(predicate) | (定義)+(述語) | だからdefinitionの部分はいらない | |
attr | attribute | 属性 | 属性を持たせる |
attr synonym(型); ::同じ意味のシンボル antonym(型); ::反対の意味のシンボル
あるmodeと別の属性(attribute)をもつmodeを組み合わせて新しいデータタイプの熟語を作り出せる
cluster 型1 型2 existence proof ~ end;
演算子作成(functor):n個の変数を組み合わせてある変数を作る記号を定義する
func A 演算子 B ※definitionのendまでは、演算子をitで表す