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 #) というように使用する