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 | ||| The eliminator for the `Void` type.
16 | public export
17 | void : (0 x : Void) -> a
18 | void _ impossible
19 |
20 | export
21 | Uninhabited Void where
22 |   uninhabited = id
23 |
24 | ||| Use an absurd assumption to discharge a proof obligation.
25 | ||| @ t some empty type
26 | ||| @ a the goal type
27 | ||| @ h the contradictory hypothesis
28 | public export
29 | absurd : Uninhabited t => (h : t) -> a
30 | absurd h = void (uninhabited h)
31 |
32 | public export
33 | Uninhabited (True = False) where
34 |   uninhabited Refl impossible
35 |
36 | public export
37 | Uninhabited (False = True) where
38 |   uninhabited Refl impossible
39 |