Data.Singletons.Bool

Contents

• Data.Type.Bool and .Equality

Synopsis

• data SBool b where
  • STrue :: SBool True
  • SFalse :: SBool False
• class SBoolI b where
• 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
• sboolEqRefl :: forall a b. SBoolI (a == b) => Maybe (a :~: b)
• trivialRefl :: () :~: ()

Documentation

Data.Type.Bool and .Equality