Idris2Doc : Data.Bool.Rewrite
Reexports
import public Data.BoolDefinitions
swapOr : (0 p : (Bool -> Type)) -> p (x || Delay y) -> p (y || Delay x)- Totality: total
Visibility: public export orSame : (0 p : (Bool -> Type)) -> p (x || Delay x) -> p x- Totality: total
Visibility: public export orTrue : (0 p : (Bool -> Type)) -> p (x || Delay True) -> p True- Totality: total
Visibility: public export orFalse : (0 p : (Bool -> Type)) -> p (x || Delay False) -> p x- Totality: total
Visibility: public export swapAnd : (0 p : (Bool -> Type)) -> p (x && Delay y) -> p (y && Delay x)- Totality: total
Visibility: public export andSame : (0 p : (Bool -> Type)) -> p (x && Delay x) -> p x- Totality: total
Visibility: public export andTrue : (0 p : (Bool -> Type)) -> p (x && Delay True) -> p x- Totality: total
Visibility: public export andFalse : (0 p : (Bool -> Type)) -> p (x && Delay False) -> p False- Totality: total
Visibility: public export