Add instance Uninhabited _|_
commit8dc49a9b3200544683c3363483772f737c647cf5
authorBrian McKenna <brian@brianmckenna.org>
dateSun 13 Apr 2014, 22:23 (13 years ago)
parent16f7da4
libs/prelude/Prelude/Uninhabited.idr+3
@@ -8,6 +8,9 @@ class Uninhabited t where
88 ||| @ t the uninhabited type
99 total uninhabited : t -> _|_
1010
11+instance Uninhabited _|_ where
12+ uninhabited a = a
13+
1114||| Use an absurd assumption to discharge a proof obligation
1215||| @ t some empty type
1316||| @ a the goal type