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

[Michael Nedzelsky <MichaelNedzelsky@yandex.ru>]

Hi Grzegorz,

> 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
>           )
>      )

Thanks a lot! It makes things more clear.

Michael Nedzelsky


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