-- Hoogle documentation, generated by Haddock
-- See Hoogle, http://www.haskell.org/hoogle/

-- | Type level booleans
--   
--   Type level booleans.
--   
--   singletons package provides similar functionality, but it has
--   tight dependency constraints.
@package singleton-bool
@version 0.1.8

-- | Additions to Data.Type.Bool.
module Data.Singletons.Bool
data SBool (b :: Bool)
[STrue] :: SBool 'True
[SFalse] :: SBool 'False
class SBoolI (b :: Bool)
sbool :: SBoolI b => SBool b

-- | Convert an SBool to the corresponding Bool.
fromSBool :: forall (b :: Bool). SBool b -> Bool

-- | Convert a normal Bool to an SBool, passing it into a
--   continuation.
--   
--   
--   >>> withSomeSBool True fromSBool
--   True
--   
withSomeSBool :: Bool -> (forall (b :: Bool). () => SBool b -> r) -> r

-- | Reflect to term-level.
--   
--   
--   >>> reflectBool (Proxy :: Proxy 'True)
--   True
--   
reflectBool :: forall (b :: Bool) proxy. SBoolI b => proxy b -> Bool

-- | Reify Bool to type-level.
--   
--   
--   >>> reifyBool True reflectBool
--   True
--   
reifyBool :: Bool -> (forall (b :: Bool). SBoolI b => Proxy b -> r) -> r

-- | Decidable equality.
--   
--   
--   >>> decShow (discreteBool :: Dec ('True :~: 'True))
--   "Yes Refl"
--   
discreteBool :: forall (a :: Bool) (b :: Bool). (SBoolI a, SBoolI b) => Dec (a :~: b)

-- | 
--   >>> sboolAnd STrue SFalse
--   SFalse
--   
sboolAnd :: forall (a :: Bool) (b :: Bool). SBool a -> SBool b -> SBool (a && b)
sboolOr :: forall (a :: Bool) (b :: Bool). SBool a -> SBool b -> SBool (a || b)
sboolNot :: forall (a :: Bool). SBool a -> SBool (Not a)

eqToRefl :: forall {k} (a :: k) (b :: k). (a == b) ~ 'True => a :~: b

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

-- | Useful combination of sbool and eqToRefl
sboolEqRefl :: forall k (a :: k) (b :: k). SBoolI (a == b) => Maybe (a :~: b)

trivialRefl :: () :~: ()
instance Data.Singletons.Bool.SBoolI b => Data.Boring.Boring (Data.Singletons.Bool.SBool b)
instance Data.EqP.EqP Data.Singletons.Bool.SBool
instance GHC.Classes.Eq (Data.Singletons.Bool.SBool b)
instance Data.GADT.Internal.GCompare Data.Singletons.Bool.SBool
instance Data.GADT.Internal.GEq Data.Singletons.Bool.SBool
instance Data.GADT.DeepSeq.GNFData Data.Singletons.Bool.SBool
instance Data.GADT.Internal.GRead Data.Singletons.Bool.SBool
instance Data.GADT.Internal.GShow Data.Singletons.Bool.SBool
instance Control.DeepSeq.NFData (Data.Singletons.Bool.SBool b)
instance Data.OrdP.OrdP Data.Singletons.Bool.SBool
instance GHC.Classes.Ord (Data.Singletons.Bool.SBool b)
instance Data.Singletons.Bool.SBoolI 'GHC.Types.False
instance Data.Singletons.Bool.SBoolI 'GHC.Types.True
instance GHC.Internal.Show.Show (Data.Singletons.Bool.SBool b)
