Idris2Doc : Data.Bool.Xor
- notXor : (a : Bool) -> (b : Bool) -> not (a `xor` b) = not a `xor` b
- Totality: total
- notXorCancel : (a : Bool) -> (b : Bool) -> not a `xor` not b = 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` not a = True
- Totality: total
- xorSameFalse : (b : Bool) -> b `xor` b = False
- Totality: total
- xorTrueNot : (b : Bool) -> True `xor` b = not b
- Totality: total