Idris2Doc : Prelude.Uninhabited

Prelude.Uninhabited

Definitions

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:
UninhabitedVoid
Uninhabited (True=False)
Uninhabited (False=True)
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)
uninhabited : Uninhabitedt=>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 : 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
Visibility: public export