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


-- | 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>.
--   
--   @since next
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>
--   
--   @since next
withSomeSBool :: Bool -> (forall b. SBool b -> r) -> r
reflectBool :: forall b proxy. SBoolI b => proxy b -> Bool

-- | Reify <a>Bool</a>.
--   
--   <pre>
--   &gt;&gt;&gt; reifyBool True reflectBool
--   True
--   </pre>
reifyBool :: forall r. Bool -> (forall b. SBoolI b => Proxy b -> r) -> r
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 (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
