IdrisDoc: Prelude.Uninhabited

Prelude.Uninhabited

Utilities for working with uninhabited types, to record explicit
locations for canonical proofs of emptiness. Typically, one should
use the absurd function.

absurd : Uninhabited t => (h : t) -> a

Use an absurd assumption to discharge a proof obligation

a

the goal type

t

some empty type

h

the contradictory hypothesis

interface Uninhabited 

A canonical proof that some type is empty

uninhabited : Uninhabited t => t -> Void

If I have a t, I've had a contradiction