Proof.Propositional.Inhabited

Documentation

class Inhabited a where

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.

Methods

trivial :: a

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

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 ()

Methods

trivial :: ()

Inhabited (IsTrue True)

Methods

trivial :: IsTrue True

Inhabited b => Inhabited (a -> b)

Methods

trivial :: a -> b

(Inhabited a, Inhabited b) => Inhabited (a, b)

Methods

trivial :: (a, b)

(Inhabited a, Inhabited b, Inhabited c) => Inhabited (a, b, c)

Methods

trivial :: (a, b, c)

(Inhabited a, Inhabited b, Inhabited c, Inhabited d) => Inhabited (a, b, c, d)

Methods

trivial :: (a, b, c, d)

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