Data.Singletons.Bool

Additions to Data.Type.Bool.

Documentation

data SBool (b :: Bool) where

Constructors

STrue :: SBool True

SFalse :: SBool False

class SBoolI (b :: Bool) where

Minimal complete definition

sbool

Methods

sbool :: SBool b

Instances

SBoolI False

Methods

sbool :: SBool False

SBoolI True

Methods

sbool :: SBool True

fromSBool :: SBool b -> Bool

Convert an SBool to the corresponding Bool.

@since next

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

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

>>> withSomeSBool True fromSBool
True

@since next

reflectBool :: forall b proxy. SBoolI b => proxy b -> Bool

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

Reify Bool.

>>> reifyBool True reflectBool
True

Data.Type.Bool and .Equality

These are only defined with base >= 4.7

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

Since: 0.1.1.0

eqCast :: (a == b) ~ True => a -> b

Since: 0.1.1.0

sboolEqRefl :: forall (a :: k) (b :: k). SBoolI (a == b) => Maybe (a :~: b)

Useful combination of sbool and eqToRefl

Since: 0.1.2.0

trivialRefl :: () :~: ()

Since: 0.1.1.0