On 5/26/25 07:54, Gino Giotto wrote:
For w3a, one could disambiguate using a slightly different symbol, not
already present in set.mm, like `( ph /\. ps /\. th )`.
That would be my instinct. I suppose if we find ourselves encountering
the situation where set.mm later defines /\. we could build some tooling
around declaring a token as reserved (and therefore not definable) but
I'm not sure I'd go to the trouble unless we find this happening often
enough to be annoying.
Another possibility could be to tell the exporter to automatically
replace `(w3a ph ps ch)` with `(wa (wa ph ps) ch)` everywhere before
introducing the notation. The original set.mm would not be preserved
If we are willing to give up round-tripping back to set.mm this might, I
suppose, work better just on the MM0/MM1 side (not that I know enough to
really say).
A hybrid approach would translate to `(wa (wa ph ps) ch)` with some kind
of annotation to enable round tripping but when I think of designing
that sort of annotation mechanism I'm not sure it ends up really
different from the /\. solution.
I haven't been close enough to MM0/MM1 to have a fully fleshed out
opinion about how to handle these issues, but I hope that it isn't
preventing people from doing things with MM0/MM1 and set.mm. At least
from a distance these issues look solvable to me.
There are also df-op `<. A , B >.` and df-ot `<. A , B , C >.` that
have the same obstacle. Dropping df-ot might be ok, but this approach
becomes problematic for definitions like df-s1, df-s2, df-s3, df-s4,
etc.. which really make statements about words shorter. I think
dropping those might not be acceptable.
ot is less used than 3an and 3or but I guess my mind first goes to
automatically translating between the metamath notation and something
which is better behaved in the ways we have been discussing. Maybe I'm
just used to the metamath notation but given that it seems like it could
be automatically translated, it doesn't seem like a major obstacle.
Now, I can think of other reasons why 3an and 3or might not be so great
(basically the overhead of having both an and 3an when they do the same
thing), but I don't know if I'd decide it based on notation.
--
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/21da50b0-1301-464d-b635-473bdee7bf36%40panix.com.
