Zulip Chat Archive

Stream: mathlib4

Topic: xor


Kevin Buzzard (Oct 24 2022 at 20:44):

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 (Oct 24 2022 at 21:19):

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)


Last updated: Dec 20 2023 at 11:08 UTC