6.2 vocabulary file の書き方
Mizar では,新たに functor を定義するときには,その functor を vocabulary file に登録する必要があります.predicates, mode を定義するときも同様に登録する必要があります.vocabulary file (.vocファイル)に,必ず行の先頭から書き始め,最初の1文字に何の名前なのかを書きます.例えば,HIDDEN.VOCですと,
HIDDEN.VOC |
Mset MReal MNat K[: L:] 0+ 32 0. R<> R< R> |
となっていて,行の先頭の1文字で何なのかを示しています.
記号 | 定義するもの | 意味 |
M | Mode | モード |
O | Functor | 関数記号 |
R | Predicate | 述語命題 |
K | Left functor bracket | 左括弧 |
L | Right functor bracket | 右括弧 |
G | Structure | 構造 |
U | Selector | 識別子 |
V | Attribute | 属性 |
行の先頭の1文字に続けて,スペースを空けずに名前を書きます.さらに functor
の場合は,そのあとにスペースを空けて,優先順位を書きます.優先順位は1から
255 までの整数で.数字が大きいほど優先順位が高くなります.省略すると64となります.
こうして vocabulary file に登録してから,article で定義します.なお vocabulary を新たに登録する場合,既に登録されていないかどうかを確認するために,
CHECKVOC [vocabulary]
として確認してください.