Merge pull request #225 from david-christiansen/uninhabited
Added typeclass for uninhabited types
commitf19d017e8854c864cec7f9286714bc992e00f6a1
authorEdwin Brady <edwin.brady@gmail.com>
dateTue 12 Mar 2013, 05:13 (14 years ago)
parent169fea1a3cd5fd
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,