On January 4, 2020 10:17:44 AM EST, Mario Carneiro <[email protected]> wrote: >On Sat, Jan 4, 2020 at 10:08 AM David A. Wheeler ><[email protected]> >wrote: > >> But changing our label conventions so that underscores are between >the >> abbreviations might be a good idea. >> >> It'd be a pain to rename everything, but that is something that can >be >> done once and could be almost entirely automated. >> > >I doubt this. Determining where the breaks are would be a highly >nontrivial >task that I would not trust to a computer without oversight, and it will >hit almost all theorems, so this is not an easy task at all.
Oh, oversight would be absolutely necessary. I think a first cut could be partly automated by noticing which symbols exist, finding their df-NAME, and splitting by NAME in that label. But it would clearly take some time. --- David A.Wheeler -- 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/3AC08BD6-927E-4851-A655-36A63401B5B3%40dwheeler.com.
