Idris2Doc : Data.Bool

Data.Bool

Definitions

notInvolutive : (x : Bool) ->not (notx) =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 (notx) =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 (notx) =True
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) =notx|| Delay (noty)
Totality: total
Visibility: export
notOrIsAnd : (x : Bool) -> (y : Bool) ->not (x|| Delay y) =notx&& Delay (noty)
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) ->nota=b
  You can reverse decidability when bool is involved.

Totality: total
Visibility: public export