Merge pull request #1063 from puffnfresh/uninhabited
Add instance Uninhabited _|_
commit029f67c2c42d01ef83abf8f905fdfcd059fcffbe
authorEdwin Brady <edwin.brady@gmail.com>
dateThu 17 Apr 2014, 11:54 (13 years ago)
parent74421328dc49a9
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