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 | Haskell2010 |
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.
Synopsis
- data family Sing :: k -> Type
- type SBool = (Sing :: Bool -> Type)
- type family If (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) = (res :: Bool) | res -> a where ...
- sNot :: Sing a -> Sing (Not a)
- type family (a :: Bool) && (b :: Bool) :: Bool where ...
- type family (a :: Bool) || (b :: Bool) :: Bool where ...
- (%&&) :: Sing a -> Sing b -> Sing (a && b)
- (%||) :: Sing a -> Sing b -> Sing (a || b)
- bool_ :: a -> a -> Bool -> a
- type family Bool_ (a :: a) (a :: a) (a :: Bool) :: a where ...
- sBool_ :: forall a (t :: a) (t :: a) (t :: Bool). 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 :: (~>) Bool Bool
- type NotSym1 (a6989586621679363899 :: Bool) = Not a6989586621679363899
- data (&&@#@$) :: (~>) Bool ((~>) Bool Bool)
- data (&&@#@$$) (a6989586621679363358 :: Bool) :: (~>) Bool Bool
- type (&&@#@$$$) (a6989586621679363358 :: Bool) (b6989586621679363359 :: Bool) = (&&) a6989586621679363358 b6989586621679363359
- data (||@#@$) :: (~>) Bool ((~>) Bool Bool)
- data (||@#@$$) (a6989586621679363599 :: Bool) :: (~>) Bool Bool
- type (||@#@$$$) (a6989586621679363599 :: Bool) (b6989586621679363600 :: Bool) = (||) a6989586621679363599 b6989586621679363600
- data Bool_Sym0 :: forall a6989586621679362607. (~>) a6989586621679362607 ((~>) a6989586621679362607 ((~>) Bool a6989586621679362607))
- data Bool_Sym1 (a6989586621679362613 :: a6989586621679362607) :: (~>) a6989586621679362607 ((~>) Bool a6989586621679362607)
- data Bool_Sym2 (a6989586621679362613 :: a6989586621679362607) (a6989586621679362614 :: a6989586621679362607) :: (~>) Bool a6989586621679362607
- type Bool_Sym3 (a6989586621679362613 :: a6989586621679362607) (a6989586621679362614 :: a6989586621679362607) (a6989586621679362615 :: Bool) = Bool_ a6989586621679362613 a6989586621679362614 a6989586621679362615
- type OtherwiseSym0 = Otherwise
The Bool
singleton
data family Sing :: k -> Type Source #
The singleton kind-indexed data family.
Instances
SDecide k => TestCoercion (Sing :: k -> Type) Source # | |
Defined in Data.Singletons.Decide | |
SDecide k => TestEquality (Sing :: k -> Type) Source # | |
Defined in Data.Singletons.Decide | |
Show (SSymbol s) Source # | |
Show (SNat n) Source # | |
Eq (Sing a) Source # | |
Ord (Sing a) Source # | |
Show (Sing z) Source # | |
(ShowSing a, ShowSing [a]) => Show (Sing z) Source # | |
ShowSing a => Show (Sing z) Source # | |
Show (Sing z) Source # | |
(ShowSing a, ShowSing b) => Show (Sing z) Source # | |
Show (Sing a) Source # | |
Show (Sing z) Source # | |
(ShowSing a, ShowSing b) => Show (Sing z) Source # | |
(ShowSing a, ShowSing b, ShowSing c) => Show (Sing z) Source # | |
(ShowSing a, ShowSing b, ShowSing c, ShowSing d) => Show (Sing z) Source # | |
(ShowSing a, ShowSing b, ShowSing c, ShowSing d, ShowSing e) => Show (Sing z) Source # | |
(ShowSing a, ShowSing b, ShowSing c, ShowSing d, ShowSing e, ShowSing f) => Show (Sing z) Source # | |
(ShowSing a, ShowSing b, ShowSing c, ShowSing d, ShowSing e, ShowSing f, ShowSing g) => Show (Sing z) Source # | |
Show (Sing z) Source # | |
ShowSing a => Show (Sing z) Source # | |
ShowSing a => Show (Sing z) Source # | |
(ShowSing a, ShowSing b) => Show (Sing z) Source # | |
ShowSing a => Show (Sing z) Source # | |
ShowSing a => Show (Sing z) Source # | |
ShowSing m => Show (Sing z) Source # | |
ShowSing (Maybe a) => Show (Sing z) Source # | |
ShowSing a => Show (Sing z) Source # | |
ShowSing (Maybe a) => Show (Sing z) Source # | |
ShowSing (Maybe a) => Show (Sing z) Source # | |
ShowSing a => Show (Sing z) Source # | |
ShowSing Bool => Show (Sing z) Source # | |
ShowSing Bool => Show (Sing z) Source # | |
ShowSing a => Show (Sing z) Source # | |
ShowSing a => Show (Sing z) Source # | |
(ShowSing a, ShowSing [a]) => Show (Sing z) Source # | |
data Sing (a :: Bool) Source # | |
data Sing (a :: Ordering) Source # | |
data Sing (n :: Nat) Source # | |
data Sing (n :: Symbol) Source # | |
Defined in Data.Singletons.TypeLits.Internal | |
data Sing (a :: ()) Source # | |
Defined in Data.Singletons.Prelude.Instances | |
data Sing (a :: Void) Source # | |
Defined in Data.Singletons.Prelude.Instances | |
data Sing (a :: All) Source # | |
data Sing (a :: Any) Source # | |
data Sing (a :: PErrorMessage) Source # | |
Defined in Data.Singletons.TypeError data Sing (a :: PErrorMessage) where
| |
data Sing (b :: [a]) Source # | |
data Sing (b :: Maybe a) Source # | |
data Sing (a :: TYPE rep) Source # | A choice of singleton for the kind Conceivably, one could generalize this instance to `Sing :: k -> Type` for
any kind We cannot produce explicit singleton values for everything in |
Defined in Data.Singletons.TypeRepTYPE | |
data Sing (b :: Min a) Source # | |
data Sing (b :: Max a) Source # | |
data Sing (b :: First a) Source # | |
data Sing (b :: Last a) Source # | |
data Sing (a :: WrappedMonoid m) Source # | |
Defined in Data.Singletons.Prelude.Semigroup.Internal data Sing (a :: WrappedMonoid m) where
| |
data Sing (b :: Option a) Source # | |
data Sing (b :: Identity a) Source # | |
data Sing (b :: First a) Source # | |
data Sing (b :: Last a) Source # | |
data Sing (b :: Dual a) Source # | |
data Sing (b :: Sum a) Source # | |
data Sing (b :: Product a) Source # | |
data Sing (b :: Down a) Source # | |
data Sing (b :: NonEmpty a) Source # | |
data Sing (c :: Either a b) Source # | |
data Sing (c :: (a, b)) Source # | |
data Sing (c :: Arg a b) Source # | |
data Sing (f :: k1 ~> k2) Source # | |
data Sing (d :: (a, b, c)) Source # | |
data Sing (c :: Const a b) Source # | |
data Sing (e :: (a, b, c, d)) Source # | |
data Sing (f :: (a, b, c, d, e)) Source # | |
data Sing (g :: (a, b, c, d, e, f)) Source # | |
data Sing (h :: (a, b, c, d, e, f, g)) Source # | |
Defined in Data.Singletons.Prelude.Instances |
Though Haddock doesn't show it, the Sing
instance above declares
constructors
SFalse :: Sing False STrue :: Sing True
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
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
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 (t :: a) (t :: a) (t :: Bool). Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply Bool_Sym0 t) t) t :: a) Source #
sOtherwise :: Sing (OtherwiseSym0 :: Bool) Source #
Defunctionalization symbols
data NotSym0 :: (~>) Bool Bool Source #
Instances
SingI NotSym0 Source # | |
SuppressUnusedWarnings NotSym0 Source # | |
Defined in Data.Singletons.Prelude.Bool suppressUnusedWarnings :: () Source # | |
type Apply NotSym0 (a6989586621679363899 :: Bool) Source # | |
Defined in Data.Singletons.Prelude.Bool |
data (&&@#@$) :: (~>) Bool ((~>) Bool Bool) infixr 3 Source #
Instances
SingI (&&@#@$) Source # | |
SuppressUnusedWarnings (&&@#@$) Source # | |
Defined in Data.Singletons.Prelude.Bool suppressUnusedWarnings :: () Source # | |
type Apply (&&@#@$) (a6989586621679363358 :: Bool) Source # | |
Defined in Data.Singletons.Prelude.Bool |
data (&&@#@$$) (a6989586621679363358 :: Bool) :: (~>) Bool Bool infixr 3 Source #
Instances
SingI x => SingI ((&&@#@$$) x :: TyFun Bool Bool -> Type) Source # | |
SuppressUnusedWarnings ((&&@#@$$) a6989586621679363358 :: TyFun Bool Bool -> Type) Source # | |
Defined in Data.Singletons.Prelude.Bool suppressUnusedWarnings :: () Source # | |
type Apply ((&&@#@$$) a6989586621679363358 :: TyFun Bool Bool -> Type) (b6989586621679363359 :: Bool) Source # | |
type (&&@#@$$$) (a6989586621679363358 :: Bool) (b6989586621679363359 :: Bool) = (&&) a6989586621679363358 b6989586621679363359 Source #
data (||@#@$) :: (~>) Bool ((~>) Bool Bool) infixr 2 Source #
Instances
SingI (||@#@$) Source # | |
SuppressUnusedWarnings (||@#@$) Source # | |
Defined in Data.Singletons.Prelude.Bool suppressUnusedWarnings :: () Source # | |
type Apply (||@#@$) (a6989586621679363599 :: Bool) Source # | |
Defined in Data.Singletons.Prelude.Bool |
data (||@#@$$) (a6989586621679363599 :: Bool) :: (~>) Bool Bool infixr 2 Source #
Instances
SingI x => SingI ((||@#@$$) x :: TyFun Bool Bool -> Type) Source # | |
SuppressUnusedWarnings ((||@#@$$) a6989586621679363599 :: TyFun Bool Bool -> Type) Source # | |
Defined in Data.Singletons.Prelude.Bool suppressUnusedWarnings :: () Source # | |
type Apply ((||@#@$$) a6989586621679363599 :: TyFun Bool Bool -> Type) (b6989586621679363600 :: Bool) Source # | |
type (||@#@$$$) (a6989586621679363599 :: Bool) (b6989586621679363600 :: Bool) = (||) a6989586621679363599 b6989586621679363600 Source #
data Bool_Sym0 :: forall a6989586621679362607. (~>) a6989586621679362607 ((~>) a6989586621679362607 ((~>) Bool a6989586621679362607)) Source #
Instances
SingI (Bool_Sym0 :: TyFun a (a ~> (Bool ~> a)) -> Type) Source # | |
SuppressUnusedWarnings (Bool_Sym0 :: TyFun a6989586621679362607 (a6989586621679362607 ~> (Bool ~> a6989586621679362607)) -> Type) Source # | |
Defined in Data.Singletons.Prelude.Bool suppressUnusedWarnings :: () Source # | |
type Apply (Bool_Sym0 :: TyFun a6989586621679362607 (a6989586621679362607 ~> (Bool ~> a6989586621679362607)) -> Type) (a6989586621679362613 :: a6989586621679362607) Source # | |
data Bool_Sym1 (a6989586621679362613 :: a6989586621679362607) :: (~>) a6989586621679362607 ((~>) Bool a6989586621679362607) Source #
Instances
SingI d => SingI (Bool_Sym1 d :: TyFun a (Bool ~> a) -> Type) Source # | |
SuppressUnusedWarnings (Bool_Sym1 a6989586621679362613 :: TyFun a6989586621679362607 (Bool ~> a6989586621679362607) -> Type) Source # | |
Defined in Data.Singletons.Prelude.Bool suppressUnusedWarnings :: () Source # | |
type Apply (Bool_Sym1 a6989586621679362613 :: TyFun a6989586621679362607 (Bool ~> a6989586621679362607) -> Type) (a6989586621679362614 :: a6989586621679362607) Source # | |
data Bool_Sym2 (a6989586621679362613 :: a6989586621679362607) (a6989586621679362614 :: a6989586621679362607) :: (~>) Bool a6989586621679362607 Source #
Instances
(SingI d1, SingI d2) => SingI (Bool_Sym2 d1 d2 :: TyFun Bool a -> Type) Source # | |
SuppressUnusedWarnings (Bool_Sym2 a6989586621679362614 a6989586621679362613 :: TyFun Bool a6989586621679362607 -> Type) Source # | |
Defined in Data.Singletons.Prelude.Bool suppressUnusedWarnings :: () Source # | |
type Apply (Bool_Sym2 a6989586621679362614 a6989586621679362613 :: TyFun Bool a -> Type) (a6989586621679362615 :: Bool) Source # | |
type Bool_Sym3 (a6989586621679362613 :: a6989586621679362607) (a6989586621679362614 :: a6989586621679362607) (a6989586621679362615 :: Bool) = Bool_ a6989586621679362613 a6989586621679362614 a6989586621679362615 Source #
type OtherwiseSym0 = Otherwise Source #