| Copyright | (C) 2013-2014 Richard Eisenberg, Jan Stolarek |
|---|---|
| License | BSD-style (see LICENSE) |
| Maintainer | Richard Eisenberg (eir@cis.upenn.edu) |
| Stability | experimental |
| Portability | non-portable |
| Safe Haskell | None |
| Language | Haskell2010 |
Data.Singletons.Prelude.Bool
Description
Defines functions and datatypes relating to the singleton for Bool,
including a singletons 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.
- data family Sing (a :: k)
- type SBool = (Sing :: Bool -> Type)
- type family If k (cond :: Bool) (tru :: k) (fls :: k) :: k where ...
- sIf :: Sing a -> Sing b -> Sing c -> Sing (If a b c)
- type family Not (a :: Bool) :: Bool where ...
- sNot :: forall t. Sing t -> Sing (Apply NotSym0 t :: Bool)
- type family (a :: Bool) :&& (a :: Bool) :: Bool where ...
- type family (a :: Bool) :|| (a :: Bool) :: Bool where ...
- (%:&&) :: forall t t. Sing t -> Sing t -> Sing (Apply (Apply (:&&$) t) t :: Bool)
- (%:||) :: forall t t. Sing t -> Sing t -> Sing (Apply (Apply (:||$) t) t :: Bool)
- bool_ :: forall a. a -> a -> Bool -> a
- type family Bool_ (a :: a) (a :: a) (a :: Bool) :: a where ...
- sBool_ :: forall t t t. Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply Bool_Sym0 t) t) t :: a)
- type family Otherwise :: Bool where ...
- sOtherwise :: Sing (OtherwiseSym0 :: Bool)
- type TrueSym0 = True
- type FalseSym0 = False
- data NotSym0 l
- type NotSym1 t = Not t
- data (:&&$) l
- data l :&&$$ l
- type (:&&$$$) t t = (:&&) t t
- data (:||$) l
- data l :||$$ l
- type (:||$$$) t t = (:||) t t
- data Bool_Sym0 l
- data Bool_Sym1 l l
- data Bool_Sym2 l l l
- type Bool_Sym3 t t t = Bool_ t t t
- type OtherwiseSym0 = Otherwise
The Bool singleton
data family Sing (a :: k) Source #
The singleton kind-indexed data family.
Instances
| data Sing Bool Source # | |
| data Sing Ordering Source # | |
| data Sing * Source # | |
| data Sing Nat Source # | |
| data Sing Symbol Source # | |
| data Sing () Source # | |
| data Sing [a0] Source # | |
| data Sing (Maybe a0) Source # | |
| data Sing (NonEmpty a0) Source # | |
| data Sing (Either a0 b0) Source # | |
| data Sing (a0, b0) Source # | |
| data Sing ((~>) k1 k2) Source # | |
| data Sing (a0, b0, c0) Source # | |
| data Sing (a0, b0, c0, d0) Source # | |
| data Sing (a0, b0, c0, d0, e0) Source # | |
| data Sing (a0, b0, c0, d0, e0, f0) Source # | |
| data Sing (a0, b0, c0, d0, e0, f0, g0) Source # | |
Though Haddock doesn't show it, the Sing instance above declares
constructors
SFalse :: Sing False STrue :: Sing True
Conditionals
type family If k (cond :: Bool) (tru :: k) (fls :: k) :: k where ... #
Type-level If. If True a b ==> a; If False a b ==> b
Singletons from Data.Bool
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 t t t. Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply Bool_Sym0 t) t) t :: a) Source #
sOtherwise :: Sing (OtherwiseSym0 :: Bool) Source #
Defunctionalization symbols
type OtherwiseSym0 = Otherwise Source #