Add a function for dealing with absurdity
Now, if a type is known to be uninhabited, `absurd` will immediately
find the proof of uninhabitedness and apply `FalseElim` to it. This can
inhabit any type.
Example:
foo : Fin Z -> String
foo f = absurd f
commit04a5b4a01d67af4e384e146a7ac478bca284be6b
authorDavid Raymond Christiansen <david@davidchristiansen.dk>
dateFri 20 Dec 2013, 23:55 (13 years ago)
parent77ab9a1
libs/base/Uninhabited.idr+3
@@ -10,3 +10,6 @@ instance Uninhabited (Fin Z) where
1010instance Uninhabited (Z = S n) where
1111 uninhabited refl impossible
1212
13+-- | Use an absurd assumption to discharge a proof obligation
14+absurd : Uninhabited t => t -> a
15+absurd t = FalseElim (uninhabited t)