6.2 Method for Writing the Vocabulary File
In Mizar, when we newly define factors, we need to register those factors into a vocabulary file. This is also true when defining predicates and mode. In the vocabulary file (.VOC file), we must always start writing from the beginning of the line and write what the name is as the first word. For example, if it is HIDDEN.VOC:
HIDDEN.VOC |
MAny |
MReal |
MNat |
K[: |
L:] |
O+ 32 |
O. |
<> |
R< |
R> |
(parts extracted)
As shown above, it displays what it is in one word at the beginning of the line.
Symbols | Things that are defined |
M | Mode |
O | Functor |
R | Predicate |
K | Left functor bracket |
L | Right functor bracket |
G | Structure |
U | Selector |
V | Attribute |
We will write names after one word in the beginning of the line without any space. In addition, for functor, we will leave a space and write in the order of precedence. The order of priority consists of integral numbers from 1 to 255 and bigger the number, higher the priority order. If we omit, it will be 64.
Thus, after registering to the vocabulary file, we will define with an article. Further, in case of newly registering a vocabulary, we need to undertake the following procedure to make sure that it is not already registered.
CHECKVOC [vocabulary]