I propose that we move symmetric difference into the main body of set.mm. It's a well-known-enough operation, and technically we now have two mathboxes that use it :-). It's not large. The move should be easy; just move everything with the symbol /_\ somewhere, say "Define basic set operations and relations".
I should note that while inclusive-or is more common *today* in math, historically exclusive-or (which is related to /_\ ) was often common. Exclusive-or was the basis of Stoic logic, not inclusive-or, and Stoic logic is the ancestor of propositional logic. Mario: > By the way, I would like to reserve the notation '^' for the number [94]. > in preparation for possible formalization of ASCII. (In MM0 I'm using _char > but 'char' is less likely to have overlapping usage.) I think formalization of ASCII is a cool idea, and I agree that '^' (and so on) would be *MUCH* better notation than _^ (and so on). If nothing else, the '...' notation is *widely* used to represent a single character, and we should prefer common notations when we can. I recommend that if you want to reserve that use - and I think you should - then you should reserve it by adding those constants to your set.mm mathbox. That way it will be immediately obvious to anyone else who sees set.mm in the future. Nobody can remember everything, and if you do that, anyone else who tries to use the term for another purpose will get an immediate error message. --- 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/E1jSvC3-0001sC-EH%40rmmprod06.runbox.
