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

Re: [mizar] Question on Mizar grammar


Hi Michael,
looks like a bug, the grammar version at http://mizar.org/language/pages/predicate-definition.html#predicate-definition with Correctness-Conditions instead of [ "correctness" Justification ";" ] seems more correct. These files are unfortunately all hand-maintained, there is no automated (e.g. bison-like) connection between them and the Mizar parser. 

Josef

On Tue, 17 Oct 2006, Michael Nedzelsky wrote:


Hi all,

I have a question about Mizar grammar.

The Mizar article XBOOLE_0.miz contains the following fragment (which begins
at line 160):

---------------------------------------------------
redefine pred X = Y means
   X c= Y & Y c= X;
 compatibility
 proof
 .....
---------------------------------------------------

But the current rule for Predicate-Definition in syntax.txt states that:

---------------------------------------------------
Predicate-Definition =
  "pred" Predicate-Pattern [ "means" Definiens ] ";"
      [ "correctness" Justification ";" ] { Predicate-Property } .
---------------------------------------------------

There is no way to get terminal "compatibility" from this rule,
so something wrong with it.

Is it correct?

Michael Nedzelsky