Idris2Doc : Data.Bool

Data.Bool

andAssociative : (x : Bool) -> (y : Bool) -> (z : Bool) -> x&& Delay (y&& Delay z) = (x&& Delay y) && Delay z
Totality: total
andCommutative : (x : Bool) -> (y : Bool) -> x&& Delay y = y&& Delay x
Totality: total
andDistribOrR : (x : Bool) -> (y : Bool) -> (z : Bool) -> x&& Delay (y|| Delay z) = (x&& Delay y) || Delay (x&& Delay z)
Totality: total
andFalseFalse : (x : Bool) -> x&& Delay False = False
Totality: total
andNotFalse : (x : Bool) -> x&& Delay (notx) = False
Totality: total
andSameNeutral : (x : Bool) -> x&& Delay x = x
Totality: total
andTrueNeutral : (x : Bool) -> x&& Delay True = x
Totality: total
invertContraBool : (a : Bool) -> (b : Bool) -> Not (a = b) -> nota = b
  You can reverse decidability when bool is involved.

Totality: total
notAndIsOr : (x : Bool) -> (y : Bool) -> not (x&& Delay y) = notx|| Delay (noty)
Totality: total
notFalseIsTrue : Not (x = False) -> x = True
Totality: total
notInvolutive : (x : Bool) -> not (notx) = x
Totality: total
notOrIsAnd : (x : Bool) -> (y : Bool) -> not (x|| Delay y) = notx&& Delay (noty)
Totality: total
notTrueIsFalse : Not (x = True) -> x = False
Totality: total
orAssociative : (x : Bool) -> (y : Bool) -> (z : Bool) -> x|| Delay (y|| Delay z) = (x|| Delay y) || Delay z
Totality: total
orCommutative : (x : Bool) -> (y : Bool) -> x|| Delay y = y|| Delay x
Totality: total
orDistribAndR : (x : Bool) -> (y : Bool) -> (z : Bool) -> x|| Delay (y&& Delay z) = (x|| Delay y) && Delay (x|| Delay z)
Totality: total
orFalseNeutral : (x : Bool) -> x|| Delay False = x
Totality: total
orNotTrue : (x : Bool) -> x|| Delay (notx) = True
Totality: total
orSameAndRightNeutral : (x : Bool) -> (y : Bool) -> x|| Delay (x&& Delay y) = x
Totality: total
orSameNeutral : (x : Bool) -> x|| Delay x = x
Totality: total
orTrueTrue : (x : Bool) -> x|| Delay True = True
Totality: total