Well, those are counterexamples to the claim that every syntax constructor uses a unique symbol, but they are not counterexamples to the claim that the mapping from ascii token to HTML display is injective, and until now this property has been maintained, in some cases even when this goes against the traditional notation; pi the constant vs the prime pi function come to mind.
I think that underlining would be the most appropriate distinguishing mark in this case, since we already use underlined versions to indicate "class" versions of set functions, it seems natural that it could be used for the set extension of the integer function. Mario On Sun, Aug 30, 2020 at 9:56 AM Norman Megill <[email protected]> wrote: > 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 > <https://groups.google.com/d/msgid/metamath/a0864256-f905-4253-a14e-f87de312791en%40googlegroups.com?utm_medium=email&utm_source=footer> > . > -- 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/CAFXXJSvX7BU9NgitoPz9QGREcNCj1F0vi-Meefipmr7uoMNqSA%40mail.gmail.com.
