Hi everybody (especially Mario, given the subject!), I am working on another MM0 implementation, and I have a few doubts about the secondary parser (parsing in general is not my strong point). It is said that, in order to have uniqueness, an infixy constant should have a unique precedence. Does this mean that it is unique among the infixy constants' precedences, or among all the precedences?
set.mm0 suggests the former, because both $es.$ (infixl) and $~$ (not infixy) have precedence 40. However, it seems to me that this is enough to lose uniqueness of parsing tree: for example, $~ x es. y$ can be parsed both as $~ (x es. y)$ and as $(~ x) es. y$, according to the grammar in mm0.md. The latter had wrong types, but I believe this is not something the parser should care about (or should it?). Thanks for explaining! Giovanni. -- Giovanni Mascellani <[email protected]> Postdoc researcher - Université Libre de Bruxelles -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/9be582b9-cada-0ba8-ac39-9e47d9569b02%40gmail.com.
signature.asc
Description: OpenPGP digital signature
