Data.Bool

Definitions

notInvolutive : (x : Bool) -> not (not x) = x

Totality: total
Visibility: export

andSameNeutral : (x : Bool) -> x && Delay x = x

Totality: total
Visibility: export

andFalseFalse : (x : Bool) -> x && Delay False = False

Totality: total
Visibility: export

andTrueNeutral : (x : Bool) -> x && Delay True = x

Totality: total
Visibility: export

andAssociative : (x : Bool) -> (y : Bool) -> (z : Bool) -> x && Delay (y && Delay z) = (x && Delay y) && Delay z

Totality: total
Visibility: export

andCommutative : (x : Bool) -> (y : Bool) -> x && Delay y = y && Delay x

Totality: total
Visibility: export

andNotFalse : (x : Bool) -> x && Delay (not x) = False

Totality: total
Visibility: export

orSameNeutral : (x : Bool) -> x || Delay x = x

Totality: total
Visibility: export

orFalseNeutral : (x : Bool) -> x || Delay False = x

Totality: total
Visibility: export

orTrueTrue : (x : Bool) -> x || Delay True = True

Totality: total
Visibility: export

orAssociative : (x : Bool) -> (y : Bool) -> (z : Bool) -> x || Delay (y || Delay z) = (x || Delay y) || Delay z

Totality: total
Visibility: export

orCommutative : (x : Bool) -> (y : Bool) -> x || Delay y = y || Delay x

Totality: total
Visibility: export

orNotTrue : (x : Bool) -> x || Delay (not x) = True

Totality: total
Visibility: export

orBothFalse : (0 _ : x || Delay y = False) -> (x = False, y = False)

Totality: total
Visibility: export

orSameAndRightNeutral : (x : Bool) -> (y : Bool) -> x || Delay (x && Delay y) = x

Totality: total
Visibility: export

andDistribOrR : (x : Bool) -> (y : Bool) -> (z : Bool) -> x && Delay (y || Delay z) = (x && Delay y) || Delay (x && Delay z)

Totality: total
Visibility: export

orDistribAndR : (x : Bool) -> (y : Bool) -> (z : Bool) -> x || Delay (y && Delay z) = (x || Delay y) && Delay (x || Delay z)

Totality: total
Visibility: export

notAndIsOr : (x : Bool) -> (y : Bool) -> not (x && Delay y) = not x || Delay (not y)

Totality: total
Visibility: export

notOrIsAnd : (x : Bool) -> (y : Bool) -> not (x || Delay y) = not x && Delay (not y)

Totality: total
Visibility: export

notTrueIsFalse : Not (x = True) -> x = False

Totality: total
Visibility: export

notFalseIsTrue : Not (x = False) -> x = True

Totality: total
Visibility: export

invertContraBool : (a : Bool) -> (b : Bool) -> Not (a = b) -> not a = b

  You can reverse decidability when bool is involved.

Totality: total
Visibility: public export