Since this is a somewhat large change (well in terms of the number of
lines of set.mm/iset.mm affected anyway, if not conceptually), I should
probably ask on the mailing list what people think of the proposed
rename of all the labels now containing "mpt2" for maps-to-operation to
"mpo". Details at https://github.com/metamath/set.mm/pull/3354 and the
one sentence rationale is that "2" does not convey anything meaningful,
but "o" stands for "operation" and thus makes sense here.
This was originally brought up by Norm and there has been a lot of
discussion over the years about what to rename it to but (as far as I
noticed) no sentiment in favor of keeping mpt2 .
So far on this particular github issue we have one message of support
and one message which I think is support (or perhaps an alternate
suggestion). Since the github issue has been open for 3 days now I guess
it is time to think in terms of merging it and getting started on the
(large) number of follow up pull requests which I have in mind
submitting once we have agreement on the new naming convention.
--
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/100313ad-e9a5-c983-8c3e-cec34b586626%40panix.com.
