Thank you. I'm pretty sure that was the message I was thinking of. It
sounds like the separate symbols for ordinal less than and less than or
equal were very early (well before anything which is in git, which
starts with something Norm called set.mm.1998-03-16-from-vax).
On 7/21/22 23:24, savask wrote:
>I remember Norm wrote a message to the mailing list (which I'm not
sure how to find) about why we use e. and C_ for ordinal less than and
ordinal no greater than, rather than having, say, <o and <_o (I think
he even said we tried the latter for a while).
I think you mean the following post of Norm about philosophy and goals
of set.mm:
https://groups.google.com/g/metamath/c/mnkBQV1_cXc/m/zz4C8_2KAAAJ The
paragraph "rules for introducing new definitions" is especially relevant.
--
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/13af2ad6-951d-4d34-918a-9ab46d4fb01an%40googlegroups.com
<https://groups.google.com/d/msgid/metamath/13af2ad6-951d-4d34-918a-9ab46d4fb01an%40googlegroups.com?utm_medium=email&utm_source=footer>.
--
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/21420770-9bfc-d1b5-5937-34f018c96b16%40panix.com.
