Vocabularies

Vocabularies define additional lexicons for Mizar Articles. Each line of a vocabulary file introduces a symbol. It begins with one character qualifier which determines the kind of the symbol, followed immediately by the representation of the defined symbol. The pair of control characters: CR, LF (DOS end of line) is a separator for the list of symbol definitions. The formal syntax of a vocabulary file is as follows:

Vocabulary-File   =  Symbol-Definition  {  ,  Symbol-Definition  }  .

Symbol-Definition   =  Symbol-Qualifier   Symbol-Representation  .

Symbol-Qualifier   =  R  |  O  |  M  |  G  |  U  |  V  |  K  |  L  .

Symbol-Representation is a string of arbitrary characters excluding control characters, space, and double colon.

Symbol-Qualifiers has the following meaning:

• R - Predicate,
• O - Functor,
• M - Mode,
• G - Structure,
• U - Selector,
• V - Attribute,
• K - Left Functor Bracket,
• L - Right Functor Bracket.

For a functor symbol an additional information may be given on vocabulary, namely, the priority of the functor. The priority is an integer between 0 and 255. If not specified, the priority is by default 64.

A vocabulary file is an ASCII, DOS-format file. Its name is the name of an article the vocabulary is attached to. The necessary extension is .voc.