singletons-2.4: A framework for generating singleton types

Data.Promotion.Prelude.Bool

Description

Defines promoted functions and datatypes relating to Bool, including a promoted version of all the definitions in Data.Bool.

Because many of these definitions are produced by Template Haskell, it is not possible to create proper Haddock documentation. Please look up the corresponding operation in Data.Bool. Also, please excuse the apparent repeated variable names. This is due to an interaction between Template Haskell and Haddock.

Synopsis

# Documentation

type family If (cond :: Bool) (tru :: k) (fls :: k) :: k where ... #

Type-level If. If True a b ==> a; If False a b ==> b

Equations

 If True (tru :: k) (fls :: k) = tru If False (tru :: k) (fls :: k) = fls

# Promoted functions from Data.Bool

type family Bool_ (a :: a) (a :: a) (a :: Bool) :: a where ... Source #

Equations

 Bool_ fls _tru False = fls Bool_ _fls tru True = tru

bool_ :: a -> a -> Bool -> a Source #

The preceding two definitions are derived from the function bool in Data.Bool. The extra underscore is to avoid name clashes with the type Bool.

type family Not (a :: Bool) = (res :: Bool) | res -> a where ... #

Type-level "not". An injective type family since 4.10.0.0.

Since: 4.7.0.0

Equations

 Not False = True Not True = False

type family (a :: Bool) && (b :: Bool) :: Bool where ... infixr 3 #

Type-level "and"

Equations

 False && a = False True && a = a a && False = False a && True = a a && a = a

type family (a :: Bool) || (b :: Bool) :: Bool where ... infixr 2 #

Type-level "or"

Equations

 False || a = a True || a = True a || False = a a || True = True a || a = a

type family Otherwise :: Bool where ... Source #

Equations

 Otherwise = TrueSym0

# Defunctionalization symbols

data NotSym0 (l :: TyFun Bool Bool) Source #

Instances
 Source # Instance detailsMethods type Apply NotSym0 (l :: Bool) Source # Instance detailstype Apply NotSym0 (l :: Bool) = Not l

type NotSym1 (t :: Bool) = Not t Source #

data (&&@#@$) (l :: TyFun Bool (TyFun Bool Bool -> Type)) Source # Instances  Source # Instance detailsMethods type Apply (&&@#@$) (l :: Bool) Source # Instance detailstype Apply (&&@#@$) (l :: Bool) = (&&@#@$$) l data (l :: Bool) &&@#@$$ (l :: TyFun Bool Bool) Source # Instances  Source # Instance detailsMethods type Apply ((&&@#@$$) l1 :: TyFun Bool Bool -> *) (l2 :: Bool) Source # Instance detailstype Apply ((&&@#@$$) l1 :: TyFun Bool Bool -> *) (l2 :: Bool) = l1 && l2 type (&&@#@$$) (t :: Bool) (t :: Bool) = (&&) t t Source # data (||@#@) (l :: TyFun Bool (TyFun Bool Bool -> Type)) Source # Instances  Source # Instance detailsMethods type Apply (||@#@) (l :: Bool) Source # Instance detailstype Apply (||@#@) (l :: Bool) = (||@#@$$) l data (l :: Bool) ||@#@$$(l :: TyFun Bool Bool) Source # Instances  Source # Instance detailsMethods type Apply ((||@#@$$) l1 :: TyFun Bool Bool -> *) (l2 :: Bool) Source # Instance detailstype Apply ((||@#@$$) l1 :: TyFun Bool Bool -> *) (l2 :: Bool) = l1 || l2 type (||@#@$$$) (t :: Bool) (t :: Bool) = (||) t t Source #

data Bool_Sym0 (l :: TyFun a6989586621679289682 (TyFun a6989586621679289682 (TyFun Bool a6989586621679289682 -> Type) -> Type)) Source #

Instances
 SuppressUnusedWarnings (Bool_Sym0 :: TyFun a6989586621679289682 (TyFun a6989586621679289682 (TyFun Bool a6989586621679289682 -> Type) -> Type) -> *) Source # Instance detailsMethods type Apply (Bool_Sym0 :: TyFun a6989586621679289682 (TyFun a6989586621679289682 (TyFun Bool a6989586621679289682 -> Type) -> Type) -> *) (l :: a6989586621679289682) Source # Instance detailstype Apply (Bool_Sym0 :: TyFun a6989586621679289682 (TyFun a6989586621679289682 (TyFun Bool a6989586621679289682 -> Type) -> Type) -> *) (l :: a6989586621679289682) = Bool_Sym1 l

data Bool_Sym1 (l :: a6989586621679289682) (l :: TyFun a6989586621679289682 (TyFun Bool a6989586621679289682 -> Type)) Source #

Instances
 SuppressUnusedWarnings (Bool_Sym1 :: a6989586621679289682 -> TyFun a6989586621679289682 (TyFun Bool a6989586621679289682 -> Type) -> *) Source # Instance detailsMethods type Apply (Bool_Sym1 l1 :: TyFun a6989586621679289682 (TyFun Bool a6989586621679289682 -> Type) -> *) (l2 :: a6989586621679289682) Source # Instance detailstype Apply (Bool_Sym1 l1 :: TyFun a6989586621679289682 (TyFun Bool a6989586621679289682 -> Type) -> *) (l2 :: a6989586621679289682) = Bool_Sym2 l1 l2

data Bool_Sym2 (l :: a6989586621679289682) (l :: a6989586621679289682) (l :: TyFun Bool a6989586621679289682) Source #

Instances
 SuppressUnusedWarnings (Bool_Sym2 :: a6989586621679289682 -> a6989586621679289682 -> TyFun Bool a6989586621679289682 -> *) Source # Instance detailsMethods type Apply (Bool_Sym2 l1 l2 :: TyFun Bool a -> *) (l3 :: Bool) Source # Instance detailstype Apply (Bool_Sym2 l1 l2 :: TyFun Bool a -> *) (l3 :: Bool) = Bool_ l1 l2 l3

type Bool_Sym3 (t :: a6989586621679289682) (t :: a6989586621679289682) (t :: Bool) = Bool_ t t t Source #