Data.Singletons.Bool

Contents

• Data.Type.Bool and .Equality

Description

Synopsis

• data SBool (b :: Bool) where
  • STrue :: SBool True
  • SFalse :: SBool False
• 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 True fromSBool
True

>>> reifyBool True reflectBool
True

Data.Type.Bool and .Equality