Re: [mizar] Question on parsing term expression with "qua".

[Josef Urban <urban@ktilinux.ms.mff.cuni.cz>]

On Wed, 1 Nov 2006, Michael Nedzelsky wrote:

> Hi Josef,
>
> First of all, thanks for the answer!
>
> > I have not looked at the actual Mizar parser code for this (and do not
> > know it at the moment). I'd like to ask Andrzej (the chairman of Assoc. of
> > Mizar Users) if I can answer here public questions like this by looking at
> > the Mizar code (I promised not to publish it six years ago). Andrzej?
>
> I think that the rules like this is the part of language definition (like the
> overloading rules in C++, for example), and I hope that the language
> defintion is open, though the pascal code for parser is closed. :)

It's a bit unclear, since the language definition is only available in the 
pascal code, and there is the additional question whether e.g. the 
proof-checking procedure is a part of "language definition". But Grzegorz 
apparently shares your opinion, so unless Andrzej says something else, 
I'll feel free to provide such info by looking at the pascal code too.

Josef