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.

Minimal complete definition

Nothing

Methods

eliminate :: a -> x

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

Instances

Empty Void

Defined in Proof.Propositional.Empty

Methods

eliminate :: Void -> x

Empty (IsTrue 'False)

Defined in Proof.Propositional

Methods

eliminate :: IsTrue 'False -> x

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

Defined in Proof.Propositional

Methods

eliminate :: (a -> b) -> x

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

Defined in Proof.Propositional.Empty

Methods

eliminate :: Either a b -> x

Empty ('False :~: 'True)

Defined in Proof.Propositional

Methods

eliminate :: ('False :~: 'True) -> x

Empty ('True :~: 'False)

Defined in Proof.Propositional

Methods

eliminate :: ('True :~: 'False) -> x

Empty ('LT :~: 'EQ)

Defined in Proof.Propositional

Methods

eliminate :: ('LT :~: 'EQ) -> x

Empty ('LT :~: 'GT)

Defined in Proof.Propositional

Methods

eliminate :: ('LT :~: 'GT) -> x

Empty ('EQ :~: 'LT)

Defined in Proof.Propositional

Methods

eliminate :: ('EQ :~: 'LT) -> x

Empty ('EQ :~: 'GT)

Defined in Proof.Propositional

Methods

eliminate :: ('EQ :~: 'GT) -> x

Empty ('GT :~: 'LT)

Defined in Proof.Propositional

Methods

eliminate :: ('GT :~: 'LT) -> x

Empty ('GT :~: 'EQ)

Defined in Proof.Propositional

Methods

eliminate :: ('GT :~: 'EQ) -> x

Empty (() :~: Int)

Defined in Proof.Propositional

Methods

eliminate :: (() :~: Int) -> x

Empty (0 :~: 1)

Defined in Proof.Propositional

Methods

eliminate :: (0 :~: 1) -> 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