Safe Haskell	None
Language	Haskell2010

Data.Singletons.Bool

Contents

Data.Type.Dec
Data.Type.Bool and .Equality

Description

Additions to Data.Type.Bool .

Synopsis

data SBool (b :: Bool ) where
- STrue :: SBool ' True
- SFalse :: SBool ' False
class SBoolI (b :: Bool ) where
- sbool :: SBool b
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 #

Constructors

STrue :: SBool ' True
SFalse :: SBool ' False

Instances

Instances details

Eq ( SBool b) Source #	Since: 0.1.5
Instance details Defined in Data.Singletons.Bool Methods (==) :: SBool b -> SBool b -> Bool Source # (/=) :: SBool b -> SBool b -> Bool Source #
Ord ( SBool b) Source #	Since: 0.1.5
Instance details Defined in Data.Singletons.Bool Methods compare :: SBool b -> SBool b -> Ordering Source # (<) :: SBool b -> SBool b -> Bool Source # (<=) :: SBool b -> SBool b -> Bool Source # (>) :: SBool b -> SBool b -> Bool Source # (>=) :: SBool b -> SBool b -> Bool Source # max :: SBool b -> SBool b -> SBool b Source # min :: SBool b -> SBool b -> SBool b Source #
Show ( SBool b) Source #	Since: 0.1.5
Instance details Defined in Data.Singletons.Bool Methods showsPrec :: Int -> SBool b -> ShowS Source # show :: SBool b -> String Source # showList :: [ SBool b] -> ShowS Source #

class SBoolI (b :: Bool ) where Source #

Methods

sbool :: SBool b Source #

Instances

Instances details

SBoolI ' False Source #
Instance details Defined in Data.Singletons.Bool Methods sbool :: SBool ' False Source #
SBoolI ' True Source #
Instance details Defined in Data.Singletons.Bool Methods sbool :: SBool ' True Source #

fromSBool :: SBool b -> Bool Source #

Convert an SBool to the corresponding Bool .

Since: 0.1.4

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

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

>>> withSomeSBool True fromSBool
True

Since: 0.1.4

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

sboolAnd :: SBool a -> SBool b -> SBool (a && b) Source #

>>> sboolAnd STrue SFalse
SFalse

sboolOr :: SBool a -> SBool b -> SBool (a || b) Source #

sboolNot :: SBool a -> SBool ( Not a) Source #

eqToRefl :: (a == b) ~ ' True => a :~: b Source #

Since: 0.1.1.0

eqCast :: (a == b) ~ ' True => a -> b Source #

Since: 0.1.1.0

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

Useful combination of sbool and eqToRefl

Since: 0.1.2.0

trivialRefl :: () :~: () Source #

Since: 0.1.1.0