[Date Prev][Date Next] [Chronological] [Thread] [Top]

Re: [mizar] Mizar lexicon



Hi Michael,

On Mon, 9 Oct 2006, Michael Nedzelsky wrote:

Hi all.

I have read the following document http://www.mizar.org/language/lexicon.html
and there are some details which I want to understand more precisely.

Questions:

1) Are property names reserved words? The property name "symmetry"
also presents in the list of reserved words, but the other property
names doesn't.

You're absolutely right. This web page hasn't been updated systematically
for some time and it doesn't reflect all relatively recent changes, including properties. The most "accurate" list of Mizar reserved words and special symbols can be retrieved from the file $MIZFILES/mizar.dct, as this is what Mizar actually uses to initiate its parsing. There one may also find reserved words which are still planned to be implemented (e.g. '...' or 'according'), but in this 'unofficial' way disallowed to be used as symbols for the time being.

Notes:

1) The reserved word "requirements" is out of order in the list of the
reserved words. (May be I am too pedantic...)

2) The vocabulary HIDDEN contains symbol "<>", which is listed as
special symbol. It seems that it must be removed from the list of the
special symbols (all the other special symbols are not vocabulary symbols).

Right, again. The '<>' symbol is now an ordinary antonym for specially treated '=', so it's not a special symbol any more.

I'll fix the page tomorrow, so the mirrors should have it corrected in two days. Surely it's also high time to remove several MS-DOS remnants from
this page ;-)

Thanks for the report.

Adam Naumowicz

======================================================================
Department of Applied Logic            fax. +48 (85) 745-7662
Institute of Computer Science          tel. +48 (85) 745-7559 (office)
University of Bialystok                e-mail: adamn@mizar.org
Sosnowa 64, 15-887 Bialystok, Poland   http://math.uwb.edu.pl/~adamn/
======================================================================