I agree with your proposals. Benoît On Thursday, July 14, 2022 at 7:16:37 AM UTC+2 Alexander van der Vekens wrote:
> 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/9803cb19-e49f-4987-a573-4a0da1580376n%40googlegroups.com.
