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?.
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
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 metamath+unsubscr...@googlegroups.com.
To view this discussion on the web visit
https://groups.google.com/d/msgid/metamath/a41d8438-f5cb-4a8e-90d8-b8cd4022f868%40googlegroups.com.
