I want to take up a topic raised by Norm in 2014 about using upper case in
labels, see
https://groups.google.com/g/metamath/c/Z_ERHq4knJg/m/cbUarfKEQqoJ):
*I notice that you use upper case in some labels. So far, almost all labels
are lower case for ease of typing, although this is the convention more
than a prohibition. Others may wish to discuss this.*
>From my point of view, we should have such a convention, and we should
document this in the "Convention" section 17.1.1 in set.mm ("theorem" ~
conventions-label <http://us2.metamath.org/mpeuni/conventions-label.html>).
There are, however, documented exceptions: the suffixes OLD, ALT and ALTV.
Another, not yet documented exception is using the suffix "N" for theorems
with tag "(New usage is discouraged.)" (593 occurrences in set.mm, but all
in Norm's mathbox). I would suggest that this is OK in mathboxes, but
should not be used in the main body of set.mm.
Maybe upper case should be allowed in mathboxes in genereal (see also
~rntrclfvOAI), but not in the main body (except the above mentioned
exceptions).
--
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/40715857-0df0-4543-a8a7-01ed140ec9d2n%40googlegroups.com.
