0 | module Prelude.Uninhabited
 1 |
 2 | import Builtin
 3 | import Prelude.Basics
 4 |
 5 | %default total
 6 |
 7 | ||| A canonical proof that some type is empty.
 8 | public export
 9 | interface Uninhabited t where
10 |   constructor MkUninhabited
11 |   ||| If I have a t, I've had a contradiction.
12 |   ||| @ t the uninhabited type
13 |   uninhabited : t -> Void
14 |
15 | %extern
16 | prim__void : (0 x : Void) -> a
17 |
18 | ||| The eliminator for the `Void` type.
19 | public export
20 | void : (0 x : Void) -> a
21 | void = prim__void
22 |
23 | export
24 | Uninhabited Void where
25 |   uninhabited = id
26 |
27 | ||| Use an absurd assumption to discharge a proof obligation.
28 | ||| @ t some empty type
29 | ||| @ a the goal type
30 | ||| @ h the contradictory hypothesis
31 | public export
32 | absurd : Uninhabited t => (h : t) -> a
33 | absurd h = void (uninhabited h)
34 |
35 | public export
36 | Uninhabited (True = False) where
37 |   uninhabited Refl impossible
38 |
39 | public export
40 | Uninhabited (False = True) where
41 |   uninhabited Refl impossible
42 |