-- 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 :: SBool b -> Bool -- | Convert a normal Bool to an SBool, passing it into a -- continuation. -- --
--   >>> withSomeSBool True fromSBool
--   True
--   
withSomeSBool :: Bool -> (forall b. SBool b -> r) -> r -- | Reflect to term-level. -- --
--   >>> reflectBool (Proxy :: Proxy 'True)
--   True
--   
reflectBool :: forall b proxy. SBoolI b => proxy b -> Bool -- | Reify Bool to type-level. -- --
--   >>> reifyBool True reflectBool
--   True
--   
reifyBool :: forall r. Bool -> (forall b. SBoolI b => Proxy b -> r) -> r -- | Decidable equality. -- --
--   >>> decShow (discreteBool :: Dec ('True :~: 'True))
--   "Yes Refl"
--   
discreteBool :: forall a b. (SBoolI a, SBoolI b) => Dec (a :~: b) -- |
--   >>> sboolAnd STrue SFalse
--   SFalse
--   
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 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 Data.Singletons.Bool.SBoolI b => Data.Boring.Boring (Data.Singletons.Bool.SBool b) 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) instance Control.DeepSeq.NFData (Data.Singletons.Bool.SBool b) instance Data.GADT.Internal.GEq Data.Singletons.Bool.SBool instance Data.GADT.Internal.GCompare Data.Singletons.Bool.SBool instance Data.GADT.DeepSeq.GNFData Data.Singletons.Bool.SBool instance Data.GADT.Internal.GShow Data.Singletons.Bool.SBool instance Data.GADT.Internal.GRead Data.Singletons.Bool.SBool instance Data.EqP.EqP Data.Singletons.Bool.SBool instance Data.OrdP.OrdP Data.Singletons.Bool.SBool