On Monday, April 27, 2020 at 1:01:56 AM UTC-4, Mario Carneiro wrote: > >> 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'
On Mon, Apr 27, 2020 at 7:35 AM Norman Megill <[email protected]> wrote: > > Maybe I missed something in this thread, but what is the purpose of > > formalizing ASCII? Is this something that eventually might be added to > > set.mm?. On Mon, 27 Apr 2020 18:10:05 -0700, Mario Carneiro <[email protected]> wrote: > While I have no > immediate plans to move this to set.mm, this is a possibility, and it also > shows an example of a mathematically reasonable use of ASCII formalization, > which may come up in set.mm in another form (e.g. metamath in metamath). All by itself that's a potentially interesting use (metamath in metamath). Norman Megill: > > Our informal convention has been to prefix non-italic letters with > > underscore, like _i, so _<letter> will clash with a few that already > > exist. How about a single quote prefix, 'a 'b 'c ... like in Lisp 'foo to > > abbreviate (quote foo)? > > That would not clash with anything in set.mm > > except ''' in AV's mathbox (for alternate function value) which could be > > changed. I like that convention. Especially since I know Lisp :-). Mario: > This also works for me. I don't think it is essential to commit to a > notation right now since I'm not actually adding these characters to set.mm, > but I wanted to make sure that others keep this use in mind. It may not be *essential*, but I think it would be wise to "reserve" these symbols for future use. Usually we add 1-2 symbols at a time, but if we ever add a representation of ASCII, we'd want to add a large set with exactly the same rule (whatever that is). If we reserve them now & don't use them, no big deal. If we don't reserve them, we might we have to do a lot of renaming and other nonsense to have a large set of symbols with a consistent convention. I'll try to make a pull request to define 'LETTER for a set, so that people will be automatically warned if they try to define an operation for some other purpose. That will "reserve" the pattern for potential use later. --- David A. Wheeler -- 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/E1jTGdZ-0006bN-Ef%40rmmprod06.runbox.
