On Sun, 12 Jul 2020 16:05:30 -0700 (PDT), "'ookami' via Metamath" <[email protected]> wrote: > ... Your idea is just one > out of a plethora of typographical aids to point out the semantics of > formulas. ...
The fact that there are other ideas doesn't make it a bad idea. This idea doesn't conflict with other ideas, either. So let's focus on the merits of the actual proposal. > My first idea is that a > processor evaluates a tag like comment with hints on how to display > otherwise difficult to read math expressions. This has to be written from > scratch. ... Feel free to write a new typographic system from scratch! That will take a lot of work. What I propose requires 0 changes to all Metamath-processing programs. It doesn't even require adding new lines to set.mm, as they're already in a mathbox; they simply need to be moved into the body. That makes my proposal *quite* different from a proposal to rewrite a typography system from scratch. It can be done today with a minor tweak to set.mm - and you're done. Even if someone creates a new typography system, having class variable names like A' available will mean that the typography system can immediately take advantage of it, instead of trying to reason those relationships out itself. Rewriting a completely different typography system is essentially unrelated to supporting variable names like A'. You can do either, both, or neither. I'm hoping that there will be agreement to supporting A' and friends; it's a trivial change with some simple benefits. --- David A. Wheeler -- 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/E1jumT6-0002Gj-HR%40rmmprod06.runbox.
