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