I second the A' proposal. Anecdotally, when working with synthetic proof generators, we've multiple times been relying on the existence of the primed class variables (despite these being defined in mathboxes).
-stan On Mon, Jul 13, 2020 at 2:37 AM David A. Wheeler <[email protected]> wrote: > > 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. -- 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/CACZd_0zQD3duDo%3D_UgTgvhFAJdMZR6DbdWa482K0JfVVY-yvtg%40mail.gmail.com.
