You can do that, but ideally this would be done as a change to the exporter, so that the theorems themselves can be stated using the notation, and also so that it stays up to date with set.mm. So the exporter will have to identify whether a notation is prefix or infix or a general notation, and there will be compromises needed on some set.mm notations that are mm0-ambiguous, like wa `( ph /\ ps )` and w3a `( ph /\ ps /\ th )`. In MM0 every notation has to start with a unique token.
On Mon, May 26, 2025 at 3:29 AM Gino Giotto <[email protected]> wrote: > > The issue is that set.mm notations are not compatible with the mm0 > notation system, and the current translation makes no attempt to translate > notations. This can be done in at least some cases automatically, but it > seems like a lot of work to tune the heuristics... > > Hmm, all I can say is that I could manually add the notations that cannot > be done automatically if they are not too many, otherwise I don't think I > can handle the tree format. I guess others would benefit as well if this > would have to be done only once. > > I don't know the language very well. Is it just about creating many lines > like "infixl wa: $/\$ prec 20;" or "prefix wex: $E.$ prec 30;" and then the > statements will be automatically prettified from that information? I'm > concerned that things will break with future set.mm updates tho. > > -- > 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/CAPKSAW4Qd15O%3DhnjnT_31oF7_FEr-7g%2BBrTnCXRKbD1VKah6BQ%40mail.gmail.com > <https://groups.google.com/d/msgid/metamath/CAPKSAW4Qd15O%3DhnjnT_31oF7_FEr-7g%2BBrTnCXRKbD1VKah6BQ%40mail.gmail.com?utm_medium=email&utm_source=footer> > . > -- 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/CAFXXJSt2AuYnLyVjahxqg%3DdPKapvCO131qYX5Xjgzvsv3%2BcrBg%40mail.gmail.com.
