Idris2Doc : Prelude.Uninhabited

Prelude.Uninhabited

Uninhabited : Type -> Type
A canonical proof that some type is empty.
Parameters: t
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)
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
Prelude.void : (0 _ : Void) -> a
The eliminator for the `Void` type.