On Sunday, August 30, 2020 at 9:38:20 AM UTC-4 Norman Megill wrote: ... > Up to now we have been careful not to overload the displayed symbols (to > my knowledge). For example, we distinguish various kinds of "+" with > subscripts, unlike most of the literature (which has a different and > complementary goal, which is to provide the reader with an informal > higher-level understanding). >
Actually that isn't strictly true: we have df-an vs. df-3an, df-sn vs. df-pr, and a few others. But I still think it would be useful to distinguish the two lcm's in some subtle way, especially since in from a grammatical point of view they are identical (both class constants) and can't be distinguished by parsing, unlike the examples I gave. An easy way is bold font for one of them, but the aesthetics of that may not be ideal. Any suggestions? Norm -- 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/a0864256-f905-4253-a14e-f87de312791en%40googlegroups.com.
