6.2 Method for Writing the Vocabulary File
In Mizar, when we newly define functors, we need to register those functors
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 |
Mset MReal MNat K[: L:] O+ 32 O. R<> R< R> |
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]