6.2 vocabulary fileの書き方

Mizar では，新たに functor を定義するときには，その functor を vocabulary file に登録する必要があります．predicates，mode を定義するときも同様に登録する必要があります．vocabulary file （.VOC ファイル）に，必ず行の先頭から書き始め，最初の1文字に 何の名前なのか を書きます．例えば，HIDDEN.VOC ですと，

HIDDEN.VOC
MAny
MReal
MNat
K[:
L:]
O+ 32
O.
<>
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]

として確認してください．