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.
signature.asc
Description: PGP signature
