Idris2Doc : Data.Bool.Xor

Data.Bool.Xor

notXor : (a : Bool) -> (b : Bool) -> not (a `xor` b) = nota `xor` b
Totality: total
notXorCancel : (a : Bool) -> (b : Bool) -> nota `xor` notb = a `xor` b
Totality: total
xor : Bool -> Bool -> Bool
Totality: total
Fixity Declaration: infixl operator, level 6
xorAssociative : (a : Bool) -> (b : Bool) -> (c : Bool) -> a `xor` (b `xor` c) = (a `xor` b) `xor` c
Totality: total
xorCommutative : (a : Bool) -> (b : Bool) -> a `xor` b = b `xor` a
Totality: total
xorFalseNeutral : (b : Bool) -> False `xor` b = b
Totality: total
xorNotTrue : (a : Bool) -> a `xor` nota = True
Totality: total
xorSameFalse : (b : Bool) -> b `xor` b = False
Totality: total
xorTrueNot : (b : Bool) -> True `xor` b = notb
Totality: total