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

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

Hi Michael,

since no one else is answering, here is an example which could clarify 
such issues (the symbols Relation and bool are used just not to define new 
vocabulary with some Foomode and Foofunc).

environ vocabularies RELAT_1; begin

definition
mode Relation means :DRel1: not contradiction;
existence;
end;

definition
let X be Relation;
mode Relation of X -> Relation means not contradiction;
correctness by DRel1;
end;

definition
let X be Relation;
func bool X -> set means it = X;
correctness;
let Y be Relation of X;
func bool Y -> Relation means it = Y;
correctness;
end;

reserve Y for Relation, V for Relation of Y, Z for Relation of V;


bool (Z qua Relation of V qua Relation) is Relation;
bool (Z qua Relation of (V qua Relation)) is Relation;
bool ((Z qua Relation of V) qua Relation) is Relation;
::>                                                 *4
::> 4: This inference is not accepted


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?

Josef

On Tue, 31 Oct 2006, Michael Nedzelsky wrote:

> Hi all,
>
> If we have the term expression like the following:
>
>  term_1 qua mode_1 of term_2 qua type_1
>
> it can be parsed in two ways:
>
> 1)   term_1 qua (mode_1 of term_2  qua type_1)
> 2)  (term_1 qua  mode_1 of term_2) qua type_1
>
> What are the current rules for disambiguation in this situation?
>
> Michael Nedzelsky
>
>
> --
> This message has been scanned for viruses and
> dangerous content by MailScanner, and is
> believed to be clean.

--
This message has been scanned for viruses and
dangerous content by MailScanner, and is
believed to be clean.