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

[Grzegorz Bancerek <bancerek@ii.pb.bialystok.pl>]

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

Hi,

the first way is used. Actually, parser is reading in this way

term_1 qua (mode_1 of (term_2 qua type_1))

term_1 qua
  [expects type]
    (mode_1 of
     [expects term-list]
       [expects term]
         (term_2 qua
           [expects type]
             type_1
         )
    )

Grzegorz