Mizar/定義
< Mizar
vocabularyファイル(*.voc)
記号定義 優先順位1~255(省略すると64)
vocabulary file | ||||
記号 | 定義型 | 意味 | existence | uniqueness |
---|---|---|---|---|
G | Structure | 構造 | ||
以後definitionが必要 | ||||
M | Mode | モード | ○ | |
O | Functor | 関数記号 | ○ | ○ |
cluster | 統合属性 | ○ | ○ | |
R | Predicate | 述語命題 | ||
K | Left functor bracket | 左括弧 | ||
L | Right functor bracket | 右括弧 | ||
U | Selector | 識別子 | ||
V | Attribute | 属性 |
structureの場合
struct NewFunc(# Syuugo->set,Func->Function #); ~.vocファイルには、以下のように記述する GNewFunc Usyuugo UFunc 証明ファイル中では the base of NewFunc(# syuugo,newFunc #) というように使用する