Copyright | (C) 2013-2014 Richard Eisenberg Jan Stolarek |
---|---|
License | BSD-style (see LICENSE) |
Maintainer | Ryan Scott |
Stability | experimental |
Portability | non-portable |
Safe Haskell | None |
Language | GHC2021 |
Defines functions and datatypes relating to the singleton for Bool
,
including singled versions 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
- type family Sing :: k -> Type
- data SBool (a :: Bool) where
- type family If (cond :: Bool) (tru :: k) (fls :: k) :: k where ...
- sIf :: forall {k} (a :: Bool) (b :: k) (c :: k). Sing a -> Sing b -> Sing c -> Sing (If a b c)
- type family Not (a :: Bool) = (res :: Bool) | res -> a where ...
- sNot :: forall (a :: Bool). Sing a -> Sing (Not a)
- type family (a :: Bool) && (b :: Bool) :: Bool where ...
- type family (a :: Bool) || (b :: Bool) :: Bool where ...
- (%&&) :: forall (a :: Bool) (b :: Bool). Sing a -> Sing b -> Sing (a && b)
- (%||) :: forall (a :: Bool) (b :: Bool). Sing a -> Sing b -> Sing (a || b)
- bool_ :: a -> a -> Bool -> a
- type family Bool_ (a1 :: a) (a2 :: a) (a3 :: Bool) :: a where ...
- sBool_ :: forall a (t1 :: a) (t2 :: a) (t3 :: Bool). Sing t1 -> Sing t2 -> Sing t3 -> Sing (Apply (Apply (Apply (Bool_Sym0 :: TyFun a (a ~> (Bool ~> a)) -> Type) t1) t2) t3)
- type family Otherwise :: Bool where ...
- sOtherwise :: Sing OtherwiseSym0
- type family TrueSym0 :: Bool where ...
- type family FalseSym0 :: Bool where ...
- data IfSym0 (a :: TyFun Bool (k ~> (k ~> k)))
- data IfSym1 (a6989586621679134776 :: Bool) (b :: TyFun k (k ~> k))
- data IfSym2 (a6989586621679134776 :: Bool) (a6989586621679134777 :: k) (c :: TyFun k k)
- type family IfSym3 (a6989586621679134776 :: Bool) (a6989586621679134777 :: k) (a6989586621679134778 :: k) :: k where ...
- data NotSym0 (a :: TyFun Bool Bool)
- type family NotSym1 (a6989586621679134554 :: Bool) :: Bool where ...
- data (&&@#@$) (a :: TyFun Bool (Bool ~> Bool))
- data (a6989586621679133848 :: Bool) &&@#@$$ (b :: TyFun Bool Bool)
- type family (a6989586621679133848 :: Bool) &&@#@$$$ (a6989586621679133849 :: Bool) :: Bool where ...
- data (||@#@$) (a :: TyFun Bool (Bool ~> Bool))
- data (a6989586621679134209 :: Bool) ||@#@$$ (b :: TyFun Bool Bool)
- type family (a6989586621679134209 :: Bool) ||@#@$$$ (a6989586621679134210 :: Bool) :: Bool where ...
- data Bool_Sym0 (a1 :: TyFun a (a ~> (Bool ~> a)))
- data Bool_Sym1 (a6989586621679132605 :: a) (b :: TyFun a (Bool ~> a))
- data Bool_Sym2 (a6989586621679132605 :: a) (a6989586621679132606 :: a) (c :: TyFun Bool a)
- type family Bool_Sym3 (a6989586621679132605 :: a) (a6989586621679132606 :: a) (a6989586621679132607 :: Bool) :: a where ...
- type family OtherwiseSym0 :: Bool where ...
The Bool
singleton
type family Sing :: k -> Type #
Instances
data SBool (a :: Bool) where Source #
Instances
TestCoercion SBool Source # | |
Defined in Data.Singletons.Base.Instances | |
TestEquality SBool Source # | |
Defined in Data.Singletons.Base.Instances | |
Show (SBool z) Source # | |
Eq (SBool z) Source # | |
Conditionals
type family If (cond :: Bool) (tru :: k) (fls :: k) :: k where ... #
Type-level If. If True a b
==> a
; If False a b
==> b
sIf :: forall {k} (a :: Bool) (b :: k) (c :: k). Sing a -> Sing b -> Sing c -> Sing (If a b c) Source #
Conditional over singletons
Singletons from Data.Bool
type family Not (a :: Bool) = (res :: Bool) | res -> a where ... #
Type-level "not". An injective type family since 4.10.0.0
.
@since base-4.7.0.0
(%&&) :: forall (a :: Bool) (b :: Bool). Sing a -> Sing b -> Sing (a && b) infixr 3 Source #
Conjunction of singletons
(%||) :: forall (a :: Bool) (b :: Bool). Sing a -> Sing b -> Sing (a || b) infixr 2 Source #
Disjunction of singletons
The following are derived from the function bool
in Data.Bool
. The extra
underscore is to avoid name clashes with the type Bool
.
sBool_ :: forall a (t1 :: a) (t2 :: a) (t3 :: Bool). Sing t1 -> Sing t2 -> Sing t3 -> Sing (Apply (Apply (Apply (Bool_Sym0 :: TyFun a (a ~> (Bool ~> a)) -> Type) t1) t2) t3) Source #
Defunctionalization symbols
data IfSym0 (a :: TyFun Bool (k ~> (k ~> k))) Source #
Instances
SingI (IfSym0 :: TyFun Bool (k ~> (k ~> k)) -> Type) Source # | |
SuppressUnusedWarnings (IfSym0 :: TyFun Bool (k ~> (k ~> k)) -> Type) Source # | |
Defined in Data.Bool.Singletons suppressUnusedWarnings :: () # | |
type Apply (IfSym0 :: TyFun Bool (k ~> (k ~> k)) -> Type) (a6989586621679134776 :: Bool) Source # | |
data IfSym1 (a6989586621679134776 :: Bool) (b :: TyFun k (k ~> k)) Source #
Instances
SingI1 (IfSym1 :: Bool -> TyFun k (k ~> k) -> Type) Source # | |
SingI c => SingI (IfSym1 c :: TyFun k (k ~> k) -> Type) Source # | |
SuppressUnusedWarnings (IfSym1 a6989586621679134776 :: TyFun k (k ~> k) -> Type) Source # | |
Defined in Data.Bool.Singletons suppressUnusedWarnings :: () # | |
type Apply (IfSym1 a6989586621679134776 :: TyFun k (k ~> k) -> Type) (a6989586621679134777 :: k) Source # | |
data IfSym2 (a6989586621679134776 :: Bool) (a6989586621679134777 :: k) (c :: TyFun k k) Source #
Instances
SingI2 (IfSym2 :: Bool -> k2 -> TyFun k2 k2 -> Type) Source # | |
SingI c => SingI1 (IfSym2 c :: k1 -> TyFun k1 k1 -> Type) Source # | |
(SingI c, SingI t) => SingI (IfSym2 c t :: TyFun k k -> Type) Source # | |
Defined in Data.Bool.Singletons | |
SuppressUnusedWarnings (IfSym2 a6989586621679134776 a6989586621679134777 :: TyFun k k -> Type) Source # | |
Defined in Data.Bool.Singletons suppressUnusedWarnings :: () # | |
type Apply (IfSym2 a6989586621679134776 a6989586621679134777 :: TyFun k k -> Type) (a6989586621679134778 :: k) Source # | |
type family IfSym3 (a6989586621679134776 :: Bool) (a6989586621679134777 :: k) (a6989586621679134778 :: k) :: k where ... Source #
data NotSym0 (a :: TyFun Bool Bool) Source #
Instances
SingI NotSym0 Source # | |
Defined in Data.Bool.Singletons | |
SuppressUnusedWarnings NotSym0 Source # | |
Defined in Data.Bool.Singletons suppressUnusedWarnings :: () # | |
type Apply NotSym0 (a6989586621679134554 :: Bool) Source # | |
Defined in Data.Bool.Singletons |
data (&&@#@$) (a :: TyFun Bool (Bool ~> Bool)) infixr 3 Source #
Instances
SingI (&&@#@$) Source # | |
Defined in Data.Bool.Singletons | |
SuppressUnusedWarnings (&&@#@$) Source # | |
Defined in Data.Bool.Singletons suppressUnusedWarnings :: () # | |
type Apply (&&@#@$) (a6989586621679133848 :: Bool) Source # | |
Defined in Data.Bool.Singletons |
data (a6989586621679133848 :: Bool) &&@#@$$ (b :: TyFun Bool Bool) infixr 3 Source #
Instances
SingI x => SingI ((&&@#@$$) x :: TyFun Bool Bool -> Type) Source # | |
Defined in Data.Bool.Singletons | |
SuppressUnusedWarnings ((&&@#@$$) a6989586621679133848 :: TyFun Bool Bool -> Type) Source # | |
Defined in Data.Bool.Singletons suppressUnusedWarnings :: () # | |
type Apply ((&&@#@$$) a6989586621679133848 :: TyFun Bool Bool -> Type) (a6989586621679133849 :: Bool) Source # | |
type family (a6989586621679133848 :: Bool) &&@#@$$$ (a6989586621679133849 :: Bool) :: Bool where ... infixr 3 Source #
data (||@#@$) (a :: TyFun Bool (Bool ~> Bool)) infixr 2 Source #
Instances
SingI (||@#@$) Source # | |
Defined in Data.Bool.Singletons | |
SuppressUnusedWarnings (||@#@$) Source # | |
Defined in Data.Bool.Singletons suppressUnusedWarnings :: () # | |
type Apply (||@#@$) (a6989586621679134209 :: Bool) Source # | |
Defined in Data.Bool.Singletons |
data (a6989586621679134209 :: Bool) ||@#@$$ (b :: TyFun Bool Bool) infixr 2 Source #
Instances
SingI x => SingI ((||@#@$$) x :: TyFun Bool Bool -> Type) Source # | |
Defined in Data.Bool.Singletons | |
SuppressUnusedWarnings ((||@#@$$) a6989586621679134209 :: TyFun Bool Bool -> Type) Source # | |
Defined in Data.Bool.Singletons suppressUnusedWarnings :: () # | |
type Apply ((||@#@$$) a6989586621679134209 :: TyFun Bool Bool -> Type) (a6989586621679134210 :: Bool) Source # | |
type family (a6989586621679134209 :: Bool) ||@#@$$$ (a6989586621679134210 :: Bool) :: Bool where ... infixr 2 Source #
data Bool_Sym0 (a1 :: TyFun a (a ~> (Bool ~> a))) Source #
Instances
SingI (Bool_Sym0 :: TyFun a (a ~> (Bool ~> a)) -> Type) Source # | |
SuppressUnusedWarnings (Bool_Sym0 :: TyFun a (a ~> (Bool ~> a)) -> Type) Source # | |
Defined in Data.Bool.Singletons suppressUnusedWarnings :: () # | |
type Apply (Bool_Sym0 :: TyFun a (a ~> (Bool ~> a)) -> Type) (a6989586621679132605 :: a) Source # | |
data Bool_Sym1 (a6989586621679132605 :: a) (b :: TyFun a (Bool ~> a)) Source #
Instances
SingI1 (Bool_Sym1 :: a -> TyFun a (Bool ~> a) -> Type) Source # | |
SingI d => SingI (Bool_Sym1 d :: TyFun a (Bool ~> a) -> Type) Source # | |
Defined in Data.Bool.Singletons | |
SuppressUnusedWarnings (Bool_Sym1 a6989586621679132605 :: TyFun a (Bool ~> a) -> Type) Source # | |
Defined in Data.Bool.Singletons suppressUnusedWarnings :: () # | |
type Apply (Bool_Sym1 a6989586621679132605 :: TyFun a (Bool ~> a) -> Type) (a6989586621679132606 :: a) Source # | |
data Bool_Sym2 (a6989586621679132605 :: a) (a6989586621679132606 :: a) (c :: TyFun Bool a) Source #
Instances
SingI2 (Bool_Sym2 :: a -> a -> TyFun Bool a -> Type) Source # | |
SingI d => SingI1 (Bool_Sym2 d :: a -> TyFun Bool a -> Type) Source # | |
(SingI d1, SingI d2) => SingI (Bool_Sym2 d1 d2 :: TyFun Bool a -> Type) Source # | |
Defined in Data.Bool.Singletons | |
SuppressUnusedWarnings (Bool_Sym2 a6989586621679132605 a6989586621679132606 :: TyFun Bool a -> Type) Source # | |
Defined in Data.Bool.Singletons suppressUnusedWarnings :: () # | |
type Apply (Bool_Sym2 a6989586621679132605 a6989586621679132606 :: TyFun Bool a -> Type) (a6989586621679132607 :: Bool) Source # | |
type family Bool_Sym3 (a6989586621679132605 :: a) (a6989586621679132606 :: a) (a6989586621679132607 :: Bool) :: a where ... Source #
type family OtherwiseSym0 :: Bool where ... Source #