Hi Wolf, On Saturday, January 4, 2020 at 11:40:11 AM UTC+1, ookami wrote: > > ... > As for the naming conventions (I reply to Norm's related answer here as > well), > my first impulse is 'why not having both?'. What about alias names beside > the current shorthand form (saving typing (errors)), say a descriptive > display > name, that is used on the web page on demand. And is found in a search > instruction as well. > > This goes in the direction of my previous post, see https://groups.google.com/d/msg/metamath/XPYuatviNV0/R7iGhHynDQAJ
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/d848182f-3328-44c5-a243-13b1bc1b87e5%40googlegroups.com.
