xor for Bool

Stream: mathlib4

[Ruben Van de Velde]

Is there actually an instance for xor on Bool in lean4?

[Mario Carneiro]

I don't think so (assuming you mean the ^^^ operator). You can use != though

[Yury G. Kudryashov]

But you don't have nice defeq for !=

[Mario Carneiro]

you should?

[Mario Carneiro]

-- it computes on literals
example : (true != true) = false := rfl
example : (true != false) = true := rfl
example : (false != true) = true := rfl
example : (false != false) = false := rfl

-- but there are no partial evaluation lucky defeqs
example : (true != a) = !a := rfl -- fail
example : (a != true) = !a := rfl -- fail
example : (a != false) = a := rfl -- fail
example : (false != a) = a := rfl -- fail

[Kevin Buzzard]

I ported xor -- it's in Mathlib.Init.Data.Bool.Basic.

[Yury G. Kudryashov]

Should we use != instead?

[Yury G. Kudryashov]

@Mario Carneiro Sorry, I didn't realize that you're talking about !=, not ≠.

[Yury G. Kudryashov]

Or define Xor instances for Bool and Prop?