On Sunday, January 5, 2020 at 6:23:22 PM UTC+1, Norman Megill wrote: > > 2. It will be a huge amount of work to add 30K acronym keys. Actually it > could be phased in slowly over a long period of time by interested people, > and we could have whatever tool just process labels that have acronym keys > and ignore the rest, until all statements have a key and we decide to make > it mandatory. > > I agree with Norm that introducing such new concepts like acronyms/keys or titles/names for theorems must be realized step by step. Whether their usage should be mandatory for new theorems very early must be discussed (advantage: consistency, no need for subsequent rework; disadvantage: may not be easy for people who want to contribute). The tools processing the new information can either ignore theorems without that information (as Norm said) or can use other information temporarily, e.g. the tooltips can continue to use the first part of the comment).
Alexander -- 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/899bf8f5-39c4-4af5-b1df-551085bd5c51%40googlegroups.com.
