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
data SBool (b :: Bool ) where Source #
Instances
Eq ( SBool b) Source # |
Since: 0.1.5 |
Ord ( SBool b) Source # |
Since: 0.1.5 |
Defined in Data.Singletons.Bool |
|
Show ( SBool b) Source # |
Since: 0.1.5 |
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 reflectBool
True
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