`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