[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