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 (not x) = 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) -> not a = b
  You can reverse decidability when bool is involved.

  Totality: total
notAndIsOr : (x : Bool) -> (y : Bool) -> not (x && Delay y) = not x || Delay (not y)
  Totality: total
notFalseIsTrue : Not (x = False) -> x = True
  Totality: total
notInvolutive : (x : Bool) -> not (not x) = x
  Totality: total
notOrIsAnd : (x : Bool) -> (y : Bool) -> not (x || Delay y) = not x && Delay (not y)
  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 (not x) = 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