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]

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