Data.Singletons.Bool

Additions to Data.Type.Bool.

Documentation

data SBool (b :: Bool) where

Constructors

STrue :: SBool 'True

SFalse :: SBool 'False

Instances

EqP SBool

Since: 0.1.7

Defined in Data.Singletons.Bool

Methods

eqp :: forall (a :: k) (b :: k). SBool a -> SBool b -> Bool

GNFData SBool

Since: 0.1.6

Defined in Data.Singletons.Bool

Methods

grnf :: forall (a :: k). SBool a -> ()

GCompare SBool

Since: 0.1.6

Defined in Data.Singletons.Bool

Methods

gcompare :: forall (a :: k) (b :: k). SBool a -> SBool b -> GOrdering a b

GEq SBool

>>> geq STrue STrue
Just Refl

>>> geq STrue SFalse
Nothing

Since: 0.1.6

Defined in Data.Singletons.Bool

Methods

geq :: forall (a :: k) (b :: k). SBool a -> SBool b -> Maybe (a :~: b)

GRead SBool

>>> readsPrec 0 "Some STrue" :: [(Some SBool, String)]
[(Some STrue,"")]

>>> readsPrec 0 "Some SFalse" :: [(Some SBool, String)]
[(Some SFalse,"")]

>>> readsPrec 0 "Some Else" :: [(Some SBool, String)]
[]

Since: 0.1.6

Defined in Data.Singletons.Bool

Methods

greadsPrec :: Int -> GReadS SBool

GShow SBool

>>> showsPrec 0 STrue ""
"STrue"

Since: 0.1.6

Defined in Data.Singletons.Bool

Methods

gshowsPrec :: forall (a :: k). Int -> SBool a -> ShowS

OrdP SBool

Since: 0.1.7

Defined in Data.Singletons.Bool

Methods

comparep :: forall (a :: k) (b :: k). SBool a -> SBool b -> Ordering

Show (SBool b)

Since: 0.1.5

Defined in Data.Singletons.Bool

Methods

showsPrec :: Int -> SBool b -> ShowS

show :: SBool b -> String

showList :: [SBool b] -> ShowS

SBoolI b => Boring (SBool b)

Since: 0.1.6

Defined in Data.Singletons.Bool

Methods

boring :: SBool b

NFData (SBool b)

Since: 0.1.6

Defined in Data.Singletons.Bool

Methods

rnf :: SBool b -> ()

Eq (SBool b)

Since: 0.1.5

Defined in Data.Singletons.Bool

Methods

(==) :: SBool b -> SBool b -> Bool

(/=) :: SBool b -> SBool b -> Bool

Ord (SBool b)

Since: 0.1.5

Defined in Data.Singletons.Bool

Methods

compare :: SBool b -> SBool b -> Ordering

(<) :: SBool b -> SBool b -> Bool

(<=) :: SBool b -> SBool b -> Bool

(>) :: SBool b -> SBool b -> Bool

(>=) :: SBool b -> SBool b -> Bool

max :: SBool b -> SBool b -> SBool b

min :: SBool b -> SBool b -> SBool b

class SBoolI (b :: Bool) where

Methods

sbool :: SBool b

Instances

SBoolI 'False

Defined in Data.Singletons.Bool

Methods

sbool :: SBool 'False

SBoolI 'True

Defined in Data.Singletons.Bool

Methods

sbool :: SBool 'True

fromSBool :: SBool b -> Bool

Convert an SBool to the corresponding Bool.

Since: 0.1.4

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: 0.1.4

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

Reflect to term-level.

>>> reflectBool (Proxy :: Proxy 'True)
True

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

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)

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)

>>> sboolAnd STrue SFalse
SFalse

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 k (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