Proof.Propositional.Inhabited

Documentation

class Inhabited a where

Types with at least one inhabitant, dual to Empty. | Current GHC doesn't provide selective-instance, hence we don't Empty provide instances for sum types in a generic deriving (DeriveAnyClass).

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

Since 0.4.0.0.

Methods

trivial :: a

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

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