Hi, I suggest reading https://en.wikipedia.org/wiki/Naming_convention and https://en.wikipedia.org/wiki/Naming_convention_(programming), the latter gives lists of pros and cons of possible strategies.
One interesting citation: "The choice of naming conventions can be an enormously controversial issue, with partisans of each holding theirs to be the best and others to be inferior. Colloquially, this is said to be a matter of dogma" Technically speaking, you are not reduced to just one identifier per theorem. In particular, you can provide a list of search keys, or maintain different conventions in parallel. The user picks his favorite then. Wolf -- 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/ee8ea5be-061b-4a13-8b4c-1c6cd5a5c5ed%40googlegroups.com.
