On Sat, 19 Oct 2019 09:11:36 -0700 (PDT), Benoit <[email protected]> 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/E1iLrXA-0001U0-3B%40rmmprod07.runbox.
