Prelude.Uninhabited

Definitions

interface Uninhabited : Type -> Type

  A canonical proof that some type is empty.

Parameters: t
Constructor: 

MkUninhabited

Methods:

uninhabited : t -> Void

  If I have a t, I've had a contradiction.
  @ t the uninhabited type

Implementations:

Uninhabited Void

Uninhabited (True = False)

Uninhabited (False = True)

Uninhabited (Nothing = Just x)

Uninhabited (Just x = Nothing)

Uninhabited (Yes p = No q)

Uninhabited (No p = Yes q)

Uninhabited (Left p = Right q)

Uninhabited (Right p = Left q)

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

Uninhabited a => Uninhabited b => Uninhabited (Either a b)

uninhabited : Uninhabited t => t -> Void

  If I have a t, I've had a contradiction.
  @ t the uninhabited type

Totality: total
Visibility: public export

void : (0 _ : Void) -> a

  The eliminator for the `Void` type.

Totality: total
Visibility: public export

absurd : Uninhabited t => t -> a

  Use an absurd assumption to discharge a proof obligation.
  @ t some empty type
  @ a the goal type
  @ h the contradictory hypothesis

Totality: total
Visibility: public export