| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Data.Singletons.Bool
Contents
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
- 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 (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 #
reifyBool :: forall r. Bool -> (forall b. SBoolI b => Proxy b -> r) -> r Source #
Reify Bool.
>>>reifyBool True reflectBoolTrue
Data.Type.Bool and .Equality
These are only defined with base >= 4.7
trivialRefl :: () :~: () Source #
Since: 0.1.1.0