Data.Bool.Xor

Definitions

xor : Bool -> Bool -> Bool

Totality: total
Visibility: public export
Fixity Declaration: infixl operator, level 6

xorSameFalse : (b : Bool) -> b `xor` b = False

Totality: total
Visibility: export

xorFalseNeutral : (b : Bool) -> False `xor` b = b

Totality: total
Visibility: export

xorTrueNot : (b : Bool) -> True `xor` b = not b

Totality: total
Visibility: export

notXor : (a : Bool) -> (b : Bool) -> not (a `xor` b) = not a `xor` b

Totality: total
Visibility: export

notXorCancel : (a : Bool) -> (b : Bool) -> not a `xor` not b = a `xor` b

Totality: total
Visibility: export

xorAssociative : (a : Bool) -> (b : Bool) -> (c : Bool) -> a `xor` (b `xor` c) = (a `xor` b) `xor` c

Totality: total
Visibility: export

xorCommutative : (a : Bool) -> (b : Bool) -> a `xor` b = b `xor` a

Totality: total
Visibility: export

xorNotTrue : (a : Bool) -> a `xor` not a = True

Totality: total
Visibility: export