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):ｎ個の変数を組み合わせてある変数を作る記号を定義する

func A 演算子 B
※definitionのendまでは、演算子をitで表す