See also my comments on Banoit's remarks. I think we agree on providing additional class variables in general. So how should we proceed? Shall we move all variables from Jonathan Ben-Naim's Mathbox to the main part? I think this would be too much (for the moment). Maybe we could move the class variables with one and two primes ( A' ,... , A" , ...) , and with the indices 0 and 1 (A0, ..., A1, ...) first.
On Saturday, October 19, 2019 at 6:24:53 PM UTC+2, David A. Wheeler wrote: > > On Sat, 19 Oct 2019 09:11:36 -0700 (PDT), Benoit <[email protected] > <javascript:>> wrote: > ... > > * A common habit in math is to name variables with primes or indices, > e.g. > > A' , A'' , A0 (displayed $A_0$), A1 etc. Looks like someone already did > > that (see us2.metamath.org/mpeuni/mmascii.html). > > > > * You write you prefer lower case to denote terms which are always sets, > > but I prefer to use the above "decorations" (primes and indices) to stay > > closer to other class variables. > > These are in the Mathbox for Jonathan Ben-Naim. > I also prefer the idea of using primes and indices if you want additional > variables, *especially* if they have some kind of relationship with > another variable > (e.g., A and A' are likely to be related somehow). > It's the same as usual math practice *AND* it's clear; that sounds > awesome. > > If this is the intended direction, I recommend that we look at > promoting those items from > Jonathan Ben-Naim's mathbox, under the general rule that things generally > get > promoted once someone wants to use something from someone else's mathbox. > > > * Finally, I see in your mm-comments "Usually used for representing > a..." > > but this is not enforceable and I think it is illusory to want future > > contributors (human or computer ones) to use $M$ for a matrix or $P$ for > a > > polynomial, etc. > > I'm perfectly happy to use variable name conventions if they help make > things clear. > Sure, the verifier won't enforce them, but that's not critical. > Human readers could use all the help they can get :-). > > --- 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/cb204796-ee52-46a2-a6b4-55ef8e7f5f2e%40googlegroups.com.
