mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-12-24 04:09:10 +03:00
31 lines
646 B
Idris
31 lines
646 B
Idris
|
module Prelude.Uninhabited
|
||
|
|
|
||
|
|
import Builtin
|
||
|
|
import Prelude.Basics
|
||
|
|
|
||
|
|
%default total
|
||
|
|
|
||
|
|
||| A canonical proof that some type is empty.
|
||
|
|
public export
|
||
|
|
interface Uninhabited t where
|
||
|
|
||| If I have a t, I've had a contradiction.
|
||
|
|
||| @ t the uninhabited type
|
||
|
|
uninhabited : t -> Void
|
||
|
|
|
||
|
|
||| The eliminator for the `Void` type.
|
||
|
|
%extern
|
||
|
|
public export
|
||
|
|
void : (0 x : Void) -> a
|
||
|
|
|
||
|
|
export
|
||
|
|
Uninhabited Void where
|
||
|
|
uninhabited = id
|
||
|
|
|
||
|
|
||| Use an absurd assumption to discharge a proof obligation.
|
||
|
|
||| @ t some empty type
|
||
|
|
||| @ a the goal type
|
||
|
|
||| @ h the contradictory hypothesis
|
||
|
|
public export
|
||
|
|
absurd : Uninhabited t => (h : t) -> a
|
||
|
|
absurd h = void (uninhabited h)
|