[Date Prev][Date Next]
[Chronological]
[Thread]
[Top]
Re: Vocabulary directive
On Mon, 4 May 1998, Vedasystem wrote:
> The vocabulary directive contains names
> of vocabular files (I guess, the files have the
> extension .VOC). But I can not find such files
> in the system (e.g. BOOLE.VOC).
>
> Where they are?
Public vocabularies are compressed in MML.VCB
You may use
listvoc BOOLE
to see what is on the BOOLE vocabulary. Quite useful is
findvoc <symbol that you'r looking for>
to find out on which vocabulary the symbol is introduced
>
> Or where the vocabulary information is kept?
>
Private vacabularies are kept in the DICT subdirectory of the current
directory.
> Is there a complete description of the syntax of vocabulary files?
>
I was sure that we have it somewhere, but I could not find it.
The syntax of the .VOC is quite simple. In the first colon
you put the qualifier of the symbol. They are
O for functor symbols
R for predicate symbols
M for mode symbols
G for structure symbols
U for selector symbols
V for attribute symbols
K for left functor brackets
L for right functor brackets
The representation of the symbols follows the qualifier immediately. In the
case of the functor symbols you may put the precedence (the biding
force) of it, separated by space. It is a numeral between 0 and 255.
The default value is 64.
> Thanks in advance,
You'r welcome
> Is there a glossary of basic Mizar notions , Mizar tutorials??
You may look to
http://mizar.org/language/lexicon.html
also syntax is described in
http://mizar.org/language/pages/mizar-article.html
We work on the documentation.
We may also write to Mizar User Service, the address is
mus@mizar.uw.bialystok.pl
Andrzej Trybulec