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
RPredicate
K Left functor bracket
LRight functor bracket
GStructure
USelector
VAttribute

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]