git.iko.soy/Idris-dev
on master help sign in
Added typeclass for uninhabited types
a3cd5fdDavid Christiansen
lib/Uninhabited.idrnew file+12
compare with master
unifiedsplit
@@ -0,0 +1,12 @@
1+module Uninhabited
2+
3+class Uninhabited t where
4+ total uninhabited : t -> _|_
5+
6+instance Uninhabited (Fin O) where
7+ uninhabited fO impossible
8+ uninhabited (fS f) impossible
9+
10+instance Uninhabited (O = S n) where
11+ uninhabited refl impossible
12+
lib/base.ipkg+2
@@ -15,6 +15,8 @@ modules = Builtins, Prelude, IO, System,
15
15
16 Decidable.Equality,
16 Decidable.Equality,
17
17
18+ Uninhabited,
19+
18 Language.Reflection,
20 Language.Reflection,
19
21
20 Data.Morphisms, Data.Bits, Data.Mod2, Data.Z, Data.Sign,
22 Data.Morphisms, Data.Bits, Data.Mod2, Data.Z, Data.Sign,