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:

(parts extracted)
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]