Indeed, I think that BASIC also uses "sqr" for "square root", but for most modern languages, this is "sqrt". Anyway, "sqr" is indeed ambiguous, so I would prefer that in all labels, "sqr" be replaced with "sqrt".
Another, more important, change within labels would be to replace everywhere "rng" with "ring". Indeed, "rng" might refer to "rngs", which is a common name for non-unital rings (rings that lost the "i" of "identity"). Therefore, it is ambiguous, and it might be more difficult than in the "sqr" case to deduce from a simple inspection if the given theorem refers to rngs or rings. Indeed, the most important is to be consistent with conventions, and this is why I replaced recently, for instance: imp3a --> impd exp3a --> expd con3and --> con3dimp ee10 --> mpisyl ee12an --> syl6an a5d --> ax5d (and friends) mpto1 --> mptnan mpto2 --> mptxor mtp-or --> mtpor mtp-xor --> mtpxor changed math token from "om" to "_om" changed math token from "pi" to "_pi" changed math token from "tau" to "_tau" Benoît -- 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/84dd5b37-1f40-4b7d-b3ac-907126041211%40googlegroups.com.
