-- 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.5


-- | 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 :: 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. SBool b -> r) -> r

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

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

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

-- | <pre>
--   &gt;&gt;&gt; sboolAnd STrue SFalse
--   SFalse
--   </pre>
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

-- | 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 'GHC.Types.True
instance Data.Singletons.Bool.SBoolI 'GHC.Types.False
instance GHC.Show.Show (Data.Singletons.Bool.SBool b)
instance GHC.Classes.Eq (Data.Singletons.Bool.SBool b)
instance GHC.Classes.Ord (Data.Singletons.Bool.SBool b)
