xor

Stream: mathlib4

[Kevin Buzzard]

I was about to whinge that xor should be the Bool function and not the Prop version (in my version of mathlib4 xor was a Proppy xor), but when I was composing the whinge I created a link to github and discovered that as of 19 hours ago it has been changed to Xor'. What's the point of the ' @Mario Carneiro ? I'm going to add xor on Bools in the WIP branch kbuzzard-data-bool-basic.

[Mario Carneiro]

The ', as ever, is a disambiguation marker: Xor refers to the notation typeclass from core which supplies the notation ^^^ for "bitwise XOR". I'm thinking of PR'ing to change that to XorOp instead (to make it consistent with AndOp and OrOp which have similar conflicts to deal with)