Heh, beat me by 5 seconds. Indeed, I meant 94. On Sun, Apr 26, 2020 at 6:55 PM heiphohmia via Metamath < [email protected]> wrote:
> Maybe this is just displaying my ignorance, but decimal 97 is ASCII 'a'. > Perhaps you mean't 94, which corresponds to the caret (i.e. '^')? > > Mario Carneiro <[email protected]> wrote: > > > Use '^' in ASCII, frown in presentation: Alexander (prefers a symbol, > not > > > "concat"); > > > > > > > By the way, I would like to reserve the notation '^' for the number 97, > in > > preparation for possible formalization of ASCII. (In MM0 I'm using _char > > but 'char' is less likely to have overlapping usage.) > > > > 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/39ZJ65EFIY1FP.3BA49F3SWBU0D%40wilsonb.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/CAFXXJSvv%2BhFeoT64yTV7oKpca2UQZofaTFKp-1NpLXhDHUzjUQ%40mail.gmail.com.
