Proof.Propositional.Empty

Documentation

class Empty a where

Type-class for types without inhabitants, dual to Inhabited. Current GHC doesn't provide selective-instance, hence we don't Empty provide instances for product types in a generic deriving (DeriveAnyClass).

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

Since 0.4.0.0.

Methods

eliminate :: a -> x

eliminate :: (Generic a, GEmpty (Rep a)) => a -> x

Instances

Empty Void

Methods

eliminate :: Void -> x

Empty (IsTrue False)

Methods

eliminate :: IsTrue False -> x

(Empty a, Empty b) => Empty (Either a b)

Methods

eliminate :: Either a b -> x

withEmpty :: forall a b. (a -> Void) -> (Empty a => b) -> b

Giving falsity witness by proving Void from a. See also withEmpty'.

Since 0.4.0.0

withEmpty' :: forall a b. (forall c. a -> c) -> (Empty a => b) -> b

Giving falsity witness by showing a entails everything. See also withEmpty.

Since 0.4.0.0