git.iko.soy/Idris-dev
on master help sign in
Add Uninhabited to Prelude

Fixes #859.

commit0fca527c0f6661da9b92c9916d3584f777190862 authorDavid Raymond Christiansen <david@davidchristiansen.dk> dateSat 8 Feb 2014, 11:08 (13 years ago) parent39636cf
5 files changed+4−5
compare with master
unifiedsplit
libs/base/Control/Isomorphism.idr−1 libs/base/base.ipkg−2 libs/prelude/Prelude.idr+1 libs/base/Uninhabited.idr → libs/prelude/Prelude/Uninhabited.idr+1−1 libs/prelude/prelude.ipkg+2−1
libs/base/Control/Isomorphism.idr−1
@@ -1,7 +1,6 @@
11module Control.Isomorphism
22
33import Syntax.PreorderReasoning
4−import Uninhabited
54
65%default total
76
libs/base/base.ipkg−2
@@ -10,8 +10,6 @@ modules = System,
1010
1111 Decidable.Decidable, Decidable.Order,
1212
13− Uninhabited,
14−
1513 Providers,
1614
1715 Language.Reflection, Language.Reflection.Utils, Language.Reflection.Errors,
libs/prelude/Prelude.idr+1
@@ -20,6 +20,7 @@ import Prelude.Chars
2020import Prelude.Traversable
2121import Prelude.Bits
2222import Prelude.Stream
23+import Prelude.Uninhabited
2324
2425import Decidable.Equality
2526
libs/base/Uninhabited.idr → libs/prelude/Prelude/Uninhabited.idrrenamed+1−1
@@ -1,4 +1,4 @@
1−module Uninhabited
1+module Prelude.Uninhabited
22
33class Uninhabited t where
44 total uninhabited : t -> _|_
libs/prelude/prelude.ipkg+2−1
@@ -1,13 +1,14 @@
11package prelude
22
33opts = "--nobuiltins --total"
4−modules = Builtins, Prelude, IO,
4+modules = Builtins, Prelude, IO,
55
66 Prelude.Algebra, Prelude.Basics, Prelude.Bool, Prelude.Cast,
77 Prelude.Classes, Prelude.Nat, Prelude.Fin, Prelude.List,
88 Prelude.Maybe, Prelude.Monad, Prelude.Applicative, Prelude.Either,
99 Prelude.Vect, Prelude.Strings, Prelude.Chars, Prelude.Functor,
1010 Prelude.Foldable, Prelude.Traversable, Prelude.Bits, Prelude.Stream,
11+ Prelude.Uninhabited,
1112
1213 Decidable.Equality
1314