Idris2Doc : Prelude.Uninhabited

Prelude.Uninhabited

interfaceUninhabited : 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 = Justx)
Uninhabited (Justx = Nothing)
Uninhabited (Yesp = Noq)
Uninhabited (Nop = Yesq)
Uninhabited (Leftp = Rightq)
Uninhabited (Rightp = Leftq)
Either (Uninhabiteda) (Uninhabitedb) => Uninhabited (a, b)
Uninhabiteda => Uninhabitedb => Uninhabited (Eitherab)
UninhabitedVoid
Uninhabited (True = False)
Uninhabited (False = True)
absurd : Uninhabitedt => 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 : Uninhabitedt => 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.