Idris2Doc : Prelude.Uninhabited

Prelude.Uninhabited

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 (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 Void
  
Uninhabited (True = False)
  
Uninhabited (False = True)
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
uninhabited : Uninhabited t => t -> Void
  If I have a t, I've had a contradiction.
  @ t the uninhabited type

  Totality: total
void : (0 _ : Void) -> a
  The eliminator for the `Void` type.