Copyright	(C) 2013-2014 Richard Eisenberg Jan Stolarek
License	BSD-style (see LICENSE)
Maintainer	Ryan Scott
Stability	experimental
Portability	non-portable
Safe Haskell	Safe-Inferred
Language	Haskell2010

Data.Bool.Singletons

Contents

The Bool singleton
Conditionals
Singletons from Data.Bool
Defunctionalization symbols

Description

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 :: Bool -> Type where
- SFalse :: SBool ('False :: Bool)
- STrue :: SBool ('True :: Bool)
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 family TrueSym0 :: Bool where ...
type family FalseSym0 :: Bool where ...
data IfSym0 :: (~>) Bool ((~>) k ((~>) k k))
data IfSym1 (a6989586621679141394 :: Bool) :: (~>) k ((~>) k k)
data IfSym2 (a6989586621679141394 :: Bool) (a6989586621679141395 :: k) :: (~>) k k
type family IfSym3 (a6989586621679141394 :: Bool) (a6989586621679141395 :: k) (a6989586621679141396 :: k) :: k where ...
data NotSym0 :: (~>) Bool Bool
type family NotSym1 (a6989586621679141194 :: Bool) :: Bool where ...
data (&&@#@$) :: (~>) Bool ((~>) Bool Bool)
data (&&@#@$$) (a6989586621679140549 :: Bool) :: (~>) Bool Bool
type family (a6989586621679140549 :: Bool) &&@#@$$$ (a6989586621679140550 :: Bool) :: Bool where ...
data (||@#@$) :: (~>) Bool ((~>) Bool Bool)
data (||@#@$$) (a6989586621679140880 :: Bool) :: (~>) Bool Bool
type family (a6989586621679140880 :: Bool) ||@#@$$$ (a6989586621679140881 :: Bool) :: Bool where ...
data Bool_Sym0 :: (~>) a ((~>) a ((~>) Bool a))
data Bool_Sym1 (a6989586621679139245 :: a) :: (~>) a ((~>) Bool a)
data Bool_Sym2 (a6989586621679139245 :: a) (a6989586621679139246 :: a) :: (~>) Bool a
type family Bool_Sym3 (a6989586621679139245 :: a) (a6989586621679139246 :: a) (a6989586621679139247 :: Bool) :: a where ...
type family OtherwiseSym0 :: Bool where ...

The `Bool` singleton

type family Sing :: k -> Type #

Instances

Instances details

type Sing Source #
Instance details Defined in Data.Semigroup.Singletons.Internal type Sing = SAll
type Sing Source #
Instance details Defined in Data.Semigroup.Singletons.Internal type Sing = SAny
type Sing Source #
Instance details Defined in Data.Singletons.Base.Instances type Sing = SVoid
type Sing Source #
Instance details Defined in Data.Singletons.Base.Instances type Sing = SOrdering
type Sing Source #
Instance details Defined in Data.Singletons.Base.TypeError type Sing = SErrorMessage
type Sing Source #
Instance details Defined in GHC.TypeLits.Singletons.Internal type Sing = SNat
type Sing Source #
Instance details Defined in Data.Singletons.Base.Instances type Sing = STuple0
type Sing Source #
Instance details Defined in Data.Singletons.Base.Instances type Sing = SBool
type Sing Source #
Instance details Defined in GHC.TypeLits.Singletons.Internal type Sing = SChar
type Sing Source #
Instance details Defined in GHC.TypeLits.Singletons.Internal type Sing = SSymbol
type Sing Source #
Instance details Defined in Data.Singletons.Base.Instances type Sing = SIdentity :: Identity a -> Type
type Sing Source #
Instance details Defined in Data.Monoid.Singletons type Sing = SFirst :: First a -> Type
type Sing Source #
Instance details Defined in Data.Monoid.Singletons type Sing = SLast :: Last a -> Type
type Sing Source #
Instance details Defined in Data.Ord.Singletons type Sing = SDown :: Down a -> Type
type Sing Source #
Instance details Defined in Data.Semigroup.Singletons.Internal type Sing = SFirst :: First a -> Type
type Sing Source #
Instance details Defined in Data.Semigroup.Singletons.Internal type Sing = SLast :: Last a -> Type
type Sing Source #
Instance details Defined in Data.Semigroup.Singletons.Internal type Sing = SMax :: Max a -> Type
type Sing Source #
Instance details Defined in Data.Semigroup.Singletons.Internal type Sing = SMin :: Min a -> Type
type Sing Source #
Instance details Defined in Data.Semigroup.Singletons.Internal type Sing = SWrappedMonoid :: WrappedMonoid m -> Type
type Sing Source #
Instance details Defined in Data.Semigroup.Singletons.Internal type Sing = SDual :: Dual a -> Type
type Sing Source #
Instance details Defined in Data.Semigroup.Singletons.Internal type Sing = SProduct :: Product a -> Type
type Sing Source #
Instance details Defined in Data.Semigroup.Singletons.Internal type Sing = SSum :: Sum a -> Type
type Sing Source #
Instance details Defined in Data.Singletons.Base.Instances type Sing = SNonEmpty :: NonEmpty a -> Type
type Sing Source #
Instance details Defined in Data.Singletons.Base.Instances type Sing = SMaybe :: Maybe a -> Type
type Sing Source #	A choice of singleton for the kind `TYPE rep` (for some `RuntimeRep` `rep`), an instantiation of which is the famous kind `Type`. Conceivably, one could generalize this instance to `Sing @k` for any kind `k`, and remove all other `Sing` instances. We don't adopt this design, however, since it is far more convenient in practice to work with explicit singleton values than `TypeRep`s (for instance, `TypeRep`s are more difficult to pattern match on, and require extra runtime checks). We cannot produce explicit singleton values for everything in `TYPE rep`, however, since it is an open kind, so we reach for `TypeRep` in this one particular case.
Instance details Defined in Data.Singletons.Base.TypeRepTYPE type Sing = TypeRep :: TYPE rep -> Type
type Sing Source #
Instance details Defined in Data.Singletons.Base.Instances type Sing = SList :: [a] -> Type
type Sing Source #
Instance details Defined in Data.Singletons.Base.Instances type Sing = SEither :: Either a b -> Type
type Sing Source #
Instance details Defined in Data.Proxy.Singletons type Sing = SProxy :: Proxy t -> Type
type Sing Source #
Instance details Defined in Data.Semigroup.Singletons type Sing = SArg :: Arg a b -> Type
type Sing
Instance details Defined in Data.Singletons type Sing = SWrappedSing :: WrappedSing a -> Type
type Sing
Instance details Defined in Data.Singletons type Sing = SLambda :: (k1 ~> k2) -> Type
type Sing Source #
Instance details Defined in Data.Singletons.Base.Instances type Sing = STuple2 :: (a, b) -> Type
type Sing Source #
Instance details Defined in Data.Functor.Const.Singletons type Sing = SConst :: Const a b -> Type
type Sing Source #
Instance details Defined in Data.Singletons.Base.Instances type Sing = STuple3 :: (a, b, c) -> Type
type Sing Source #
Instance details Defined in Data.Functor.Product.Singletons type Sing = SProduct :: Product f g a -> Type
type Sing Source #
Instance details Defined in Data.Functor.Sum.Singletons type Sing = SSum :: Sum f g a -> Type
type Sing Source #
Instance details Defined in Data.Singletons.Base.Instances type Sing = STuple4 :: (a, b, c, d) -> Type
type Sing Source #
Instance details Defined in Data.Functor.Compose.Singletons type Sing = SCompose :: Compose f g a -> Type
type Sing Source #
Instance details Defined in Data.Singletons.Base.Instances type Sing = STuple5 :: (a, b, c, d, e) -> Type
type Sing Source #
Instance details Defined in Data.Singletons.Base.Instances type Sing = STuple6 :: (a, b, c, d, e, f) -> Type
type Sing Source #
Instance details Defined in Data.Singletons.Base.Instances type Sing = STuple7 :: (a, b, c, d, e, f, g) -> Type

data SBool :: Bool -> Type where Source #

Constructors

SFalse :: SBool ('False :: Bool)
STrue :: SBool ('True :: Bool)

Instances

Instances details

TestCoercion SBool Source #
Instance details Defined in Data.Singletons.Base.Instances Methods testCoercion :: forall (a :: k) (b :: k). SBool a -> SBool b -> Maybe (Coercion a b) #
TestEquality SBool Source #
Instance details Defined in Data.Singletons.Base.Instances Methods testEquality :: forall (a :: k) (b :: k). SBool a -> SBool b -> Maybe (a :~: b) #
Show (SBool z) Source #
Instance details Defined in Data.Singletons.Base.Instances Methods showsPrec :: Int -> SBool z -> ShowS # show :: SBool z -> String # showList :: [SBool z] -> ShowS #

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

Equations

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

sIf :: 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

Equations

Not 'False = 'True
Not 'True = 'False

sNot :: Sing a -> Sing (Not a) Source #

Negation of a singleton

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

(%&&) :: Sing a -> Sing b -> Sing (a && b) infixr 3 Source #

Conjunction of singletons

(%||) :: 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.

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

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

Equations

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

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 #

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

Equations

Otherwise = TrueSym0

sOtherwise :: Sing (OtherwiseSym0 :: Bool) Source #

Defunctionalization symbols

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

Equations

TrueSym0 = 'True

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

Equations

FalseSym0 = 'False

data IfSym0 :: (~>) Bool ((~>) k ((~>) k k)) Source #

Instances

Instances details

SingI (IfSym0 :: TyFun Bool (k ~> (k ~> k)) -> Type) Source #
Instance details Defined in Data.Bool.Singletons Methods sing :: Sing IfSym0
SuppressUnusedWarnings (IfSym0 :: TyFun Bool (k ~> (k ~> k)) -> Type) Source #
Instance details Defined in Data.Bool.Singletons Methods suppressUnusedWarnings :: () #
type Apply (IfSym0 :: TyFun Bool (k ~> (k ~> k)) -> Type) (a6989586621679141394 :: Bool) Source #
Instance details Defined in Data.Bool.Singletons type Apply (IfSym0 :: TyFun Bool (k ~> (k ~> k)) -> Type) (a6989586621679141394 :: Bool) = IfSym1 a6989586621679141394 :: TyFun k (k ~> k) -> Type

data IfSym1 (a6989586621679141394 :: Bool) :: (~>) k ((~>) k k) Source #

Instances

Instances details

SingI1 (IfSym1 :: Bool -> TyFun k (k ~> k) -> Type) Source #
Instance details Defined in Data.Bool.Singletons Methods liftSing :: forall (x :: k1). Sing x -> Sing (IfSym1 x)
SingI c => SingI (IfSym1 c :: TyFun k (k ~> k) -> Type) Source #
Instance details Defined in Data.Bool.Singletons Methods sing :: Sing (IfSym1 c)
SuppressUnusedWarnings (IfSym1 a6989586621679141394 :: TyFun k (k ~> k) -> Type) Source #
Instance details Defined in Data.Bool.Singletons Methods suppressUnusedWarnings :: () #
type Apply (IfSym1 a6989586621679141394 :: TyFun k (k ~> k) -> Type) (a6989586621679141395 :: k) Source #
Instance details Defined in Data.Bool.Singletons type Apply (IfSym1 a6989586621679141394 :: TyFun k (k ~> k) -> Type) (a6989586621679141395 :: k) = IfSym2 a6989586621679141394 a6989586621679141395

data IfSym2 (a6989586621679141394 :: Bool) (a6989586621679141395 :: k) :: (~>) k k Source #

Instances

Instances details

SingI2 (IfSym2 :: Bool -> k2 -> TyFun k2 k2 -> Type) Source #
Instance details Defined in Data.Bool.Singletons Methods liftSing2 :: forall (x :: k1) (y :: k20). Sing x -> Sing y -> Sing (IfSym2 x y)
SingI c => SingI1 (IfSym2 c :: k1 -> TyFun k1 k1 -> Type) Source #
Instance details Defined in Data.Bool.Singletons Methods liftSing :: forall (x :: k10). Sing x -> Sing (IfSym2 c x)
(SingI c, SingI t) => SingI (IfSym2 c t :: TyFun k k -> Type) Source #
Instance details Defined in Data.Bool.Singletons Methods sing :: Sing (IfSym2 c t)
SuppressUnusedWarnings (IfSym2 a6989586621679141394 a6989586621679141395 :: TyFun k k -> Type) Source #
Instance details Defined in Data.Bool.Singletons Methods suppressUnusedWarnings :: () #
type Apply (IfSym2 a6989586621679141394 a6989586621679141395 :: TyFun k k -> Type) (a6989586621679141396 :: k) Source #
Instance details Defined in Data.Bool.Singletons type Apply (IfSym2 a6989586621679141394 a6989586621679141395 :: TyFun k k -> Type) (a6989586621679141396 :: k) = If a6989586621679141394 a6989586621679141395 a6989586621679141396

type family IfSym3 (a6989586621679141394 :: Bool) (a6989586621679141395 :: k) (a6989586621679141396 :: k) :: k where ... Source #

Equations

IfSym3 a6989586621679141394 a6989586621679141395 a6989586621679141396 = If a6989586621679141394 a6989586621679141395 a6989586621679141396

data NotSym0 :: (~>) Bool Bool Source #

Instances

Instances details

SingI NotSym0 Source #
Instance details Defined in Data.Bool.Singletons Methods sing :: Sing NotSym0
SuppressUnusedWarnings NotSym0 Source #
Instance details Defined in Data.Bool.Singletons Methods suppressUnusedWarnings :: () #
type Apply NotSym0 (a6989586621679141194 :: Bool) Source #
Instance details Defined in Data.Bool.Singletons type Apply NotSym0 (a6989586621679141194 :: Bool) = Not a6989586621679141194

type family NotSym1 (a6989586621679141194 :: Bool) :: Bool where ... Source #

Equations

NotSym1 a6989586621679141194 = Not a6989586621679141194

data (&&@#@$) :: (~>) Bool ((~>) Bool Bool) infixr 3 Source #

Instances

Instances details

SingI (&&@#@$) Source #
Instance details Defined in Data.Bool.Singletons Methods sing :: Sing (&&@#@$)
SuppressUnusedWarnings (&&@#@$) Source #
Instance details Defined in Data.Bool.Singletons Methods suppressUnusedWarnings :: () #
type Apply (&&@#@$) (a6989586621679140549 :: Bool) Source #
Instance details Defined in Data.Bool.Singletons type Apply (&&@#@$) (a6989586621679140549 :: Bool) = (&&@#@$$) a6989586621679140549

data (&&@#@$$) (a6989586621679140549 :: Bool) :: (~>) Bool Bool infixr 3 Source #

Instances

Instances details

SingI x => SingI ((&&@#@$$) x :: TyFun Bool Bool -> Type) Source #
Instance details Defined in Data.Bool.Singletons Methods sing :: Sing ((&&@#@$$) x)
SuppressUnusedWarnings ((&&@#@$$) a6989586621679140549 :: TyFun Bool Bool -> Type) Source #
Instance details Defined in Data.Bool.Singletons Methods suppressUnusedWarnings :: () #
type Apply ((&&@#@$$) a6989586621679140549 :: TyFun Bool Bool -> Type) (a6989586621679140550 :: Bool) Source #
Instance details Defined in Data.Bool.Singletons type Apply ((&&@#@$$) a6989586621679140549 :: TyFun Bool Bool -> Type) (a6989586621679140550 :: Bool) = a6989586621679140549 && a6989586621679140550

type family (a6989586621679140549 :: Bool) &&@#@$$$ (a6989586621679140550 :: Bool) :: Bool where ... infixr 3 Source #

Equations

a6989586621679140549 &&@#@$$$ a6989586621679140550 = (&&) a6989586621679140549 a6989586621679140550

data (||@#@$) :: (~>) Bool ((~>) Bool Bool) infixr 2 Source #

Instances

Instances details

SingI (\|\|@#@$) Source #
Instance details Defined in Data.Bool.Singletons Methods sing :: Sing (\|\|@#@$)
SuppressUnusedWarnings (\|\|@#@$) Source #
Instance details Defined in Data.Bool.Singletons Methods suppressUnusedWarnings :: () #
type Apply (\|\|@#@$) (a6989586621679140880 :: Bool) Source #
Instance details Defined in Data.Bool.Singletons type Apply (\|\|@#@$) (a6989586621679140880 :: Bool) = (\|\|@#@$$) a6989586621679140880

data (||@#@$$) (a6989586621679140880 :: Bool) :: (~>) Bool Bool infixr 2 Source #

Instances

Instances details

SingI x => SingI ((\|\|@#@$$) x :: TyFun Bool Bool -> Type) Source #
Instance details Defined in Data.Bool.Singletons Methods sing :: Sing ((\|\|@#@$$) x)
SuppressUnusedWarnings ((\|\|@#@$$) a6989586621679140880 :: TyFun Bool Bool -> Type) Source #
Instance details Defined in Data.Bool.Singletons Methods suppressUnusedWarnings :: () #
type Apply ((\|\|@#@$$) a6989586621679140880 :: TyFun Bool Bool -> Type) (a6989586621679140881 :: Bool) Source #
Instance details Defined in Data.Bool.Singletons type Apply ((\|\|@#@$$) a6989586621679140880 :: TyFun Bool Bool -> Type) (a6989586621679140881 :: Bool) = a6989586621679140880 \|\| a6989586621679140881

type family (a6989586621679140880 :: Bool) ||@#@$$$ (a6989586621679140881 :: Bool) :: Bool where ... infixr 2 Source #

Equations

a6989586621679140880 ||@#@$$$ a6989586621679140881 = (||) a6989586621679140880 a6989586621679140881

data Bool_Sym0 :: (~>) a ((~>) a ((~>) Bool a)) Source #

Instances

Instances details

SingI (Bool_Sym0 :: TyFun a (a ~> (Bool ~> a)) -> Type) Source #
Instance details Defined in Data.Bool.Singletons Methods sing :: Sing Bool_Sym0
SuppressUnusedWarnings (Bool_Sym0 :: TyFun a (a ~> (Bool ~> a)) -> Type) Source #
Instance details Defined in Data.Bool.Singletons Methods suppressUnusedWarnings :: () #
type Apply (Bool_Sym0 :: TyFun a (a ~> (Bool ~> a)) -> Type) (a6989586621679139245 :: a) Source #
Instance details Defined in Data.Bool.Singletons type Apply (Bool_Sym0 :: TyFun a (a ~> (Bool ~> a)) -> Type) (a6989586621679139245 :: a) = Bool_Sym1 a6989586621679139245

data Bool_Sym1 (a6989586621679139245 :: a) :: (~>) a ((~>) Bool a) Source #

Instances

Instances details

SingI1 (Bool_Sym1 :: a -> TyFun a (Bool ~> a) -> Type) Source #
Instance details Defined in Data.Bool.Singletons Methods liftSing :: forall (x :: k1). Sing x -> Sing (Bool_Sym1 x)
SingI d => SingI (Bool_Sym1 d :: TyFun a (Bool ~> a) -> Type) Source #
Instance details Defined in Data.Bool.Singletons Methods sing :: Sing (Bool_Sym1 d)
SuppressUnusedWarnings (Bool_Sym1 a6989586621679139245 :: TyFun a (Bool ~> a) -> Type) Source #
Instance details Defined in Data.Bool.Singletons Methods suppressUnusedWarnings :: () #
type Apply (Bool_Sym1 a6989586621679139245 :: TyFun a (Bool ~> a) -> Type) (a6989586621679139246 :: a) Source #
Instance details Defined in Data.Bool.Singletons type Apply (Bool_Sym1 a6989586621679139245 :: TyFun a (Bool ~> a) -> Type) (a6989586621679139246 :: a) = Bool_Sym2 a6989586621679139245 a6989586621679139246

data Bool_Sym2 (a6989586621679139245 :: a) (a6989586621679139246 :: a) :: (~>) Bool a Source #

Instances

Instances details

SingI2 (Bool_Sym2 :: a -> a -> TyFun Bool a -> Type) Source #
Instance details Defined in Data.Bool.Singletons Methods liftSing2 :: forall (x :: k1) (y :: k2). Sing x -> Sing y -> Sing (Bool_Sym2 x y)
SingI d => SingI1 (Bool_Sym2 d :: a -> TyFun Bool a -> Type) Source #
Instance details Defined in Data.Bool.Singletons Methods liftSing :: forall (x :: k1). Sing x -> Sing (Bool_Sym2 d x)
(SingI d1, SingI d2) => SingI (Bool_Sym2 d1 d2 :: TyFun Bool a -> Type) Source #
Instance details Defined in Data.Bool.Singletons Methods sing :: Sing (Bool_Sym2 d1 d2)
SuppressUnusedWarnings (Bool_Sym2 a6989586621679139245 a6989586621679139246 :: TyFun Bool a -> Type) Source #
Instance details Defined in Data.Bool.Singletons Methods suppressUnusedWarnings :: () #
type Apply (Bool_Sym2 a6989586621679139245 a6989586621679139246 :: TyFun Bool a -> Type) (a6989586621679139247 :: Bool) Source #
Instance details Defined in Data.Bool.Singletons type Apply (Bool_Sym2 a6989586621679139245 a6989586621679139246 :: TyFun Bool a -> Type) (a6989586621679139247 :: Bool) = Bool_ a6989586621679139245 a6989586621679139246 a6989586621679139247

type family Bool_Sym3 (a6989586621679139245 :: a) (a6989586621679139246 :: a) (a6989586621679139247 :: Bool) :: a where ... Source #

Equations

Bool_Sym3 a6989586621679139245 a6989586621679139246 a6989586621679139247 = Bool_ a6989586621679139245 a6989586621679139246 a6989586621679139247

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

Equations

OtherwiseSym0 = Otherwise

'False \|\| a = a
'True \|\| a = 'True
a \|\| 'False = a
a \|\| 'True = 'True
a \|\| a = a

SingI (\|\|@#@$) Source #
Instance details Defined in Data.Bool.Singletons Methods sing :: Sing (\|\|@#@$)
SuppressUnusedWarnings (\|\|@#@$) Source #
Instance details Defined in Data.Bool.Singletons Methods suppressUnusedWarnings :: () #
type Apply (\|\|@#@$) (a6989586621679140880 :: Bool) Source #
Instance details Defined in Data.Bool.Singletons type Apply (\|\|@#@$) (a6989586621679140880 :: Bool) = (\|\|@#@$$) a6989586621679140880

SingI x => SingI ((\|\|@#@$$) x :: TyFun Bool Bool -> Type) Source #
Instance details Defined in Data.Bool.Singletons Methods sing :: Sing ((\|\|@#@$$) x)
SuppressUnusedWarnings ((\|\|@#@$$) a6989586621679140880 :: TyFun Bool Bool -> Type) Source #
Instance details Defined in Data.Bool.Singletons Methods suppressUnusedWarnings :: () #
type Apply ((\|\|@#@$$) a6989586621679140880 :: TyFun Bool Bool -> Type) (a6989586621679140881 :: Bool) Source #
Instance details Defined in Data.Bool.Singletons type Apply ((\|\|@#@$$) a6989586621679140880 :: TyFun Bool Bool -> Type) (a6989586621679140881 :: Bool) = a6989586621679140880 \|\| a6989586621679140881

The Bool singleton

Instances

Instances

Conditionals

Singletons from Data.Bool

Defunctionalization symbols

Instances

Instances

Instances

Instances

Instances

Instances

Instances

Instances

Instances

Instances

Instances

The `Bool` singleton

Singletons from `Data.Bool`