On 5/30/25 12:10, Mario Carneiro wrote:
this is one of the most difficult cases in the proof of unambiguity.
See https://us.metamath.org/downloads/grammar-ambiguity.txt for more
on this
Has anyone done any work on a tool to automatically check the metamath
grammar for ambiguities? When I was encouraged to add additional syntax
I was told "oh don't worry it won't be ambiguous". I presume that was
true in the particular case which I think was probably
https://us.metamath.org/mpeuni/df-dju.html although I don't remember for
sure whether that is the only syntax I've added. Maybe this isn't quite
up there with the definition checker in terms of likely ways to
introduce unsoundness, but if we did manage to make the grammar
ambiguous it likely would have similar consequences to the things the
definition checker checks for.
--
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 visit
https://groups.google.com/d/msgid/metamath/3b59996d-72f6-4e7f-aad3-14c31b2daab5%40panix.com.
