Convention for labels in set.mm: lower case only?

[Alexander van der Vekens]

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).

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).

[Benoit]

I agree with your proposals.

Benoît