| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Data.Singletons.Bool
Description
Additions to Data.Type.Bool.
Synopsis
- data SBool (b :: Bool) where
- class SBoolI (b :: Bool) where
- fromSBool :: SBool b -> Bool
- withSomeSBool :: Bool -> (forall b. SBool b -> r) -> r
- reflectBool :: forall b proxy. SBoolI b => proxy b -> Bool
- reifyBool :: forall r. Bool -> (forall b. SBoolI b => Proxy b -> r) -> r
- discreteBool :: forall a b. (SBoolI a, SBoolI b) => Dec (a :~: b)
- sboolAnd :: SBool a -> SBool b -> SBool (a && b)
- sboolOr :: SBool a -> SBool b -> SBool (a || b)
- sboolNot :: SBool a -> SBool (Not a)
- eqToRefl :: (a == b) ~ True => a :~: b
- eqCast :: (a == b) ~ True => a -> b
- sboolEqRefl :: forall k (a :: k) (b :: k). SBoolI (a == b) => Maybe (a :~: b)
- trivialRefl :: () :~: ()
Documentation
withSomeSBool :: Bool -> (forall b. SBool b -> r) -> r Source #
reflectBool :: forall b proxy. SBoolI b => proxy b -> Bool Source #
Reflect to term-level.
>>>reflectBool (Proxy :: Proxy 'True)True
reifyBool :: forall r. Bool -> (forall b. SBoolI b => Proxy b -> r) -> r Source #
Reify Bool to type-level.
>>>reifyBool True reflectBoolTrue
Data.Type.Dec
discreteBool is available with base >= 4.7 (GHC-7.8)
discreteBool :: forall a b. (SBoolI a, SBoolI b) => Dec (a :~: b) Source #
Decidable equality.
>>>decShow (discreteBool :: Dec ('True :~: 'True))"Yes Refl"
Since: 0.1.5
Data.Type.Bool and .Equality
These are only defined with base >= 4.7
trivialRefl :: () :~: () Source #
Since: 0.1.1.0