On Mon, Jan 6, 2020 at 6:03 AM Mario Carneiro <[email protected]> wrote:
> On Sun, Jan 5, 2020 at 10:56 PM David A. Wheeler <[email protected]> > wrote: > >> On Sun, 5 Jan 2020 09:23:21 -0800 (PST), Norman Megill <[email protected]> >> wrote: >> > I also dislike the idea of have to type 3_eq_tr_4_d instead of 3eqtr4d. >> >> That's unfortunate. Okay, sounds like adding underscores to the >> labels is off the table. That's okay, I'm just trying to identify >> possible problems & possible solutions. >> >> In most cases there shouldn't be multiple acronyms, since the acronyms >> are mostly the NAME part of df-NAME. And while the ":NUMBER" will >> prevent some kinds of overlap, I think for most people the :NUMBER >> won't help understand what is being labelled. >> > > My understanding of Norm's proposal is that this is a markup feature only. > I would like to suggest the notion of alternative names. The short and unique label continues, but it can be commented with additional alternative names, what can be latter typed in GUIs to search for labels. Say... $( $j altname '3_eq_tr_4_d'; altname '2 + 2 = 4'; $) I'm not suggesting to add altnames to all set.mm initially, but a prevision of this would incentive experiments. To people who really like to have alternative names in all set.mm, external tools could then use external files to annotate the labels they most use, and a central repository could be used to post their personal altnames files to see if some consensus emerge. André -- 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/CAL1T4B1qnCP6OH44fVicJh8TadBfeJTvB%2BjCzAN_kmRkuLrKcA%40mail.gmail.com.
