Safe Haskell	None
Language	Haskell2010

Proof.Propositional.Inhabited

Synopsis

class Inhabited a where
- trivial :: a
withInhabited :: forall a b. a -> (Inhabited a => b) -> b

Documentation

class Inhabited a where Source #

Types with at least one inhabitant, dual to Empty. Currently, GHC doesn't provide a selective-instance, hence we can't generically derive Inhabited instances for sum types (i.e. by DeriveAnyClass).

To derive an instance for each concrete types, use prove.

Since 0.4.0.0.

Minimal complete definition

Nothing

Methods

trivial :: a Source #

A generic inhabitant of type a, which means that one cannot assume anything about the value of trivial except that it

is of type a, and
doesn't contain any partial values.

trivial :: (Generic a, GInhabited (Rep a)) => a Source #

A generic inhabitant of type a, which means that one cannot assume anything about the value of trivial except that it

is of type a, and
doesn't contain any partial values.

Instances

Inhabited Bool Source #
Instance details Defined in Proof.Propositional Methods trivial :: Bool Source #
Inhabited Char Source #
Instance details Defined in Proof.Propositional Methods trivial :: Char Source #
Inhabited Double Source #
Instance details Defined in Proof.Propositional Methods trivial :: Double Source #
Inhabited Float Source #
Instance details Defined in Proof.Propositional Methods trivial :: Float Source #
Inhabited Int Source #
Instance details Defined in Proof.Propositional Methods trivial :: Int Source #
Inhabited Integer Source #
Instance details Defined in Proof.Propositional Methods trivial :: Integer Source #
Inhabited Ordering Source #
Instance details Defined in Proof.Propositional Methods trivial :: Ordering Source #
Inhabited Word Source #
Instance details Defined in Proof.Propositional Methods trivial :: Word Source #
Inhabited () Source #
Instance details Defined in Proof.Propositional.Inhabited Methods trivial :: () Source #
Inhabited [a] Source #
Instance details Defined in Proof.Propositional Methods trivial :: [a] Source #
Inhabited (Maybe a) Source #
Instance details Defined in Proof.Propositional Methods trivial :: Maybe a Source #
Inhabited (Ratio Integer) Source #
Instance details Defined in Proof.Propositional Methods trivial :: Ratio Integer Source #
Inhabited (IsTrue True) Source #
Instance details Defined in Proof.Propositional Methods trivial :: IsTrue True Source #
Inhabited b => Inhabited (a -> b) Source #
Instance details Defined in Proof.Propositional.Inhabited Methods trivial :: a -> b Source #
(Inhabited a, Inhabited b) => Inhabited (a, b) Source #
Instance details Defined in Proof.Propositional.Inhabited Methods trivial :: (a, b) Source #
(Inhabited a, Inhabited b, Inhabited c) => Inhabited (a, b, c) Source #
Instance details Defined in Proof.Propositional.Inhabited Methods trivial :: (a, b, c) Source #
Inhabited (n :~: n) Source #
Instance details Defined in Proof.Propositional Methods trivial :: n :~: n Source #
(Inhabited a, Inhabited b, Inhabited c, Inhabited d) => Inhabited (a, b, c, d) Source #
Instance details Defined in Proof.Propositional.Inhabited Methods trivial :: (a, b, c, d) Source #

withInhabited :: forall a b. a -> (Inhabited a => b) -> b Source #