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

Re: [mizar] "identify" missing from mizar grammar



On Sat, 7 Apr 2007 01:31 pm, Jesse Alama wrote:
> The recent discussions of "identify" made me want to investigate it,
> so I checked on the mizar grammar page
>
>   http://wiki.mizar.org/twiki/pub/Mizar/MizarSyntax/mizar.xml
>
> Somehow "identify" is missing.  Where does it belong?

It is simply an overlook on my part. I have compared the grammar on the wiki 
with the grammar in Mizar distribution (doc/syntax.txt) by hand...
I have tried my mini-parser on MML 4.75.958, which did not contain "identify" 
constructs, so this omission was not detected.

Since the current version of the Mizar distibution contains new grammar 
(December 14, 2006), I must do the comparsion again.

By the way, the new grammar in distribution still contains errors, which I 
have corrected in wiki version.
See for example
http://mizar.uwb.edu.pl/forum/archive/0610/msg00015.html

For now,  the only way for investigation of "identify" is to check syntax.txt  
in Mizar dsitribution and examples of usage in new MML (complfld.miz, 
gr_cy_1.miz, int_3.miz etc).

Regards,
  Michael Nedzelsky