git.iko.soy/Idris-dev
on master help sign in
Add a function for dealing with absurdity
04a5b4aDavid Raymond Christiansen
libs/base/Uninhabited.idr+3
compare with master
unifiedsplit
@@ -10,3 +10,6 @@ instance Uninhabited (Fin Z) where
10instance Uninhabited (Z = S n) where
10instance Uninhabited (Z = S n) where
11 uninhabited refl impossible
11 uninhabited refl impossible
12
12
13+-- | Use an absurd assumption to discharge a proof obligation
14+absurd : Uninhabited t => t -> a
15+absurd t = FalseElim (uninhabited t)