on master help sign in
Add instance Uninhabited _|_
8dc49a9Brian McKenna
libs/prelude/Prelude/Uninhabited.idr+3
@@ -8,6 +8,9 @@ class Uninhabited t where
8 ||| @ t the uninhabited type
8 ||| @ t the uninhabited type
9 total uninhabited : t -> _|_
9 total uninhabited : t -> _|_
10
10
11+instance Uninhabited _|_ where
12+ uninhabited a = a
13+
11||| Use an absurd assumption to discharge a proof obligation
14||| Use an absurd assumption to discharge a proof obligation
12||| @ t some empty type
15||| @ t some empty type
13||| @ a the goal type
16||| @ a the goal type