-- 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.4 -- | 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. -- -- @since next fromSBool :: SBool b -> Bool -- | Convert a normal Bool to an SBool, passing it into a -- continuation. -- --
--   >>> withSomeSBool True fromSBool
--   True
--   
-- -- @since next withSomeSBool :: Bool -> (forall b. SBool b -> r) -> r reflectBool :: forall b proxy. SBoolI b => proxy b -> Bool -- | Reify Bool. -- --
--   >>> reifyBool True reflectBool
--   True
--   
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 sbool and eqToRefl 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