Merge pull request #746 from david-christiansen/absurdity
Add a function for dealing with absurdity
commitd599c0a7a1bafe04bda8c961abfb7de39d4b39eb
authorEdwin Brady <edwin.brady@gmail.com>
dateSun 22 Dec 2013, 04:38 (13 years ago)
parentabe366e04a5b4a
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)