On Mon, Apr 27, 2020 at 7:35 AM Norman Megill <[email protected]> wrote:
> 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' >> > > 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?. > I didn't explain this, but I am already using a formalization of ASCII in MM0, for example https://github.com/digama0/mm0/blob/master/examples/mm0.mm0#L405-L459 . As you can see there, it is being used in order to define the input language of MM0 so that I can make a claim about an MM0 verifier. 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). 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. > > 'h : 'e : 'l : 'l : 'o : 'sp : 'w : 'o : 'r : 'l : 'd > 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. 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/CAFXXJSt%3DbAEt1c%3Dw8VbaTbC_aKcwQzuQR0_augvqyF_NUmVoyQ%40mail.gmail.com.
