Given this discussion, I plan to keep the definitions for ">" etc. in my mathbox and drop the PR to move it into the main body of set.mm. It can still be referred to in comments, of course.
I'll probably do some minor work in my mathbox to show the utility of "definitions not in the main body". My hope is that this will convince others later that there's value in doing so. But that's for another time, and clearly not accepted at this time. --- David A. Wheeler -- 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/E1ixYun-0002Q2-7E%40rmmprod07.runbox.
