||| Utilities for working with uninhabited types, to record explicit
||| locations for canonical proofs of emptiness. Typically, one should
||| use the `absurd` function.
module Prelude.Uninhabited
import Builtins
||| A canonical proof that some type is empty
class Uninhabited t where
||| If I have a t, I've had a contradiction
||| @ t the uninhabited type
total uninhabited : t -> Void
instance Uninhabited Void where
uninhabited a = a
||| Use an absurd assumption to discharge a proof obligation
||| @ t some empty type
||| @ a the goal type
||| @ h the contradictory hypothesis
absurd : Uninhabited t => (h : t) -> a
absurd h = void (uninhabited h)