Added typeclass for uninhabited types
This typeclass can make pleasing the completion checker much easier, as well
as when using a contradiction.
commita3cd5fd0e37c64f36edae07de8e8e0c490a55734
authorDavid Christiansen <david@davidchristiansen.dk>
dateTue 12 Mar 2013, 10:57 (14 years ago)
parent169fea1
lib/Uninhabited.idrnew file+12
@@ -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,
1515
1616 Decidable.Equality,
1717
18+ Uninhabited,
19+
1820 Language.Reflection,
1921
2022 Data.Morphisms, Data.Bits, Data.Mod2, Data.Z, Data.Sign,