On Sun, Apr 26, 2020 at 9:16 PM David A. Wheeler <[email protected]> wrote:
> I think formalization of ASCII is a cool idea, and I agree that > '^' (and so on) would be *MUCH* better notation than _^ (and so on). > If nothing else, the '...' notation is *widely* used to represent a single > character, > and we should prefer common notations when we can. > I know, and this is a bigger issue for set.mm than in the mm0 databases because these are smaller and more purpose driven. One reason I went with _c notations for characters is because it is easier to read _h : _e : _l : _l : _o : __ : _w : _o : _r : _l : _d than 'h' : 'e' : 'l' : 'l' : 'o' : 'sp' : 'w' : 'o' : 'r' : 'l' : 'd' at least in monospace. But again, this is a luxury of not having a hundred competing notations from everything else in maths. For set.mm, the _c notations aren't really an option. I recommend that if you want to reserve that use - and I think you should - > then you should reserve it by adding those constants to your set.mm > mathbox. > I'd rather not, as ASCII is rather large and I don't like declaring a huge number of definitions in advance of use. Even in MM0 I've only declared about 40 or so characters from ASCII, only the ones I need in order to say what I need to. If I declare everything in advance then it's not clear where to stop, and heaven help us if we want anything from unicode. Mario -- 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/CAFXXJStG%3DMCp3Q7ojw-SGOPRdajMKwgdrq8QW68WR%2BQV3tUn0w%40mail.gmail.com.
