Modulesingleton-bool-0.1.8Haskell2010

Data.Singletons.Bool

Additions to Data.Type.Bool.

Contents

Data.Type.Dec
Data.Type.Bool and .Equality

Synopsis

data SBool
class SBoolI
value fromSBool
value withSomeSBool
value reflectBool
value reifyBool
value discreteBool
value sboolAnd
value sboolOr
value sboolNot
value eqToRefl
value eqCast
value sboolEqRefl
value trivialRefl

Packagesingleton-bool-0.1.8
Exports14
LanguageHaskell2010
LicenceBSD-3-Clause
SourceBool.hs

datadata SBool (b :: Bool) where

Constructors

STrue :: SBool 'True
SFalse :: SBool 'False

Instances12EqP, GCompare, GEq, GNFData, GRead, GShow, …

EqP SBoolDefined in singleton-bool-0.1.8 · Data.Singletons.Bool
GCompare SBoolDefined in singleton-bool-0.1.8 · Data.Singletons.Bool
GEq SBoolDefined in singleton-bool-0.1.8 · Data.Singletons.Bool
Example1 expression
```
>>> geq STrue STrueJust Refl
```
Example1 expression
```
>>> geq STrue SFalseNothing
```
GNFData SBoolDefined in singleton-bool-0.1.8 · Data.Singletons.Bool

GRead SBoolDefined in singleton-bool-0.1.8 · Data.Singletons.Bool

Example1 expression

>>> readsPrec 0 "Some STrue" :: [(Some SBool, String)][(Some STrue,"")]

Example1 expression

>>> readsPrec 0 "Some SFalse" :: [(Some SBool, String)][(Some SFalse,"")]

Example1 expression

>>> readsPrec 0 "Some Else" :: [(Some SBool, String)][]

GShow SBoolDefined in singleton-bool-0.1.8 · Data.Singletons.Bool
Example1 expression
```
>>> showsPrec 0 STrue """STrue"
```
OrdP SBoolDefined in singleton-bool-0.1.8 · Data.Singletons.Bool
Eq (SBool b)Defined in singleton-bool-0.1.8 · Data.Singletons.Bool
Ord (SBool b)Defined in singleton-bool-0.1.8 · Data.Singletons.Bool
Show (SBool b)Defined in singleton-bool-0.1.8 · Data.Singletons.Bool
NFData (SBool b)Defined in singleton-bool-0.1.8 · Data.Singletons.Bool
SBoolI b => Boring (SBool b)Defined in singleton-bool-0.1.8 · Data.Singletons.Bool

classclass SBoolI (b :: Bool) where

Methods

sbool :: SBool b

Instances2SBoolI

SBoolI 'FalseDefined in singleton-bool-0.1.8 · Data.Singletons.Bool
SBoolI 'TrueDefined in singleton-bool-0.1.8 · Data.Singletons.Bool

valuefromSBool :: SBool b -> Bool

Source#

Convert an SBool to the corresponding Bool.

valuewithSomeSBool :: Bool -> (forall (b :: Bool). SBool b -> r) -> r

Source#

Convert a normal Bool to an SBool, passing it into a continuation.

Example1 expression

>>> withSomeSBool True fromSBoolTrue

valuereflectBool :: SBoolI b => proxy b -> Bool

Source#

Reflect to term-level.

Example1 expression

>>> reflectBool (Proxy :: Proxy 'True)True

valuereifyBool :: Bool -> (forall (b :: Bool). SBoolI b => Proxy b -> r) -> r

Source#

Reify Bool to type-level.

Example1 expression

>>> reifyBool True reflectBoolTrue

Data.Type.Dec

discreteBool is available with base >= 4.7 (GHC-7.8)

valuediscreteBool :: (SBoolI a, SBoolI b) => Dec (a :~: b)

Source#

Decidable equality.

Example1 expression

>>> decShow (discreteBool :: Dec ('True :~: 'True))"Yes Refl"

Data.Type.Bool and .Equality

These are only defined with base >= 4.7

valuesboolAnd :: SBool a -> SBool b -> SBool (a && b)

Source#

Example1 expression

>>> sboolAnd STrue SFalseSFalse

valuesboolOr :: SBool a -> SBool b -> SBool (a || b)

valuesboolNot :: SBool a -> SBool (Not a)

valueeqToRefl :: (a == b) ~ 'True => a :~: b

Source#

valueeqCast :: (a == b) ~ 'True => a -> b

Source#

valuesboolEqRefl :: SBoolI (a == b) => Maybe (a :~: b)

Source#

Useful combination of sbool and eqToRefl

valuetrivialRefl :: () :~: ()

Source#