> it is being used in order to define the input language of MM0 so that I can > make a claim about an MM0 verifier
Ah, and here I had let my hopes get up that it was for formalizing Gödel's Incompleteness Theorem (which is in the Metamath 100, after all). On April 27, 2020 6:10:05 PM PDT, Mario Carneiro <[email protected]> wrote: >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. -- 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/90F66605-289E-430A-8EF2-7940543A8CFB%40panix.com.
