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


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


-- | Additions to <a>Data.Type.Bool</a>.
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 <a>SBool</a> to the corresponding <a>Bool</a>.
fromSBool :: forall (b :: Bool). SBool b -> Bool

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

-- | Reflect to term-level.
--   
--   <pre>
--   &gt;&gt;&gt; reflectBool (Proxy :: Proxy 'True)
--   True
--   </pre>
reflectBool :: forall (b :: Bool) proxy. SBoolI b => proxy b -> Bool

-- | Reify <a>Bool</a> to type-level.
--   
--   <pre>
--   &gt;&gt;&gt; reifyBool True reflectBool
--   True
--   </pre>
reifyBool :: Bool -> (forall (b :: Bool). SBoolI b => Proxy b -> r) -> r

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

-- | <pre>
--   &gt;&gt;&gt; sboolAnd STrue SFalse
--   SFalse
--   </pre>
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 <a>sbool</a> and <a>eqToRefl</a>
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)
