8b8038c · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Move Decidable.Equality to Prelude

commit8b8038cc110b90f96d500931f6517b44c373835f authorEdwin Brady <ecb10@st-andrews.ac.uk> dateThu 21 Nov 2013, 15:14 (13 years ago) parenta7f86fe

4 files changed+12−3

unifiedsplit

libs/base/base.ipkg+1−1

@@ -8,7 +8,7 @@ modules = System,

99 System.Concurrency.Raw, System.Concurrency.Process,

1010

11− Decidable.Equality, Decidable.Decidable, Decidable.Order,

11+ Decidable.Decidable, Decidable.Order,

1212

1313 Uninhabited,

1414

libs/base/Decidable/Equality.idr → libs/prelude/Decidable/Equality.idrrenamed+6−1

@@ -1,6 +1,11 @@

11module Decidable.Equality

3−import Prelude

3+import Builtins

4+import Prelude.Either

5+import Prelude.List

6+import Prelude.Vect

7+import Prelude.Fin

8+import Prelude.Maybe

510--------------------------------------------------------------------------------

611-- Utility lemmas

libs/prelude/Prelude.idr+2

@@ -19,6 +19,8 @@ import Prelude.Traversable

1919import Prelude.Bits

2020import Prelude.Stream

2121

22+import Decidable.Equality

23+

2224%access public

2325%default total

2426

libs/prelude/prelude.ipkg+3−1

@@ -7,5 +7,7 @@ modules = Builtins, Prelude, IO,

77 Prelude.List, Prelude.Maybe, Prelude.Monad, Prelude.Applicative,

88 Prelude.Either, Prelude.Vect, Prelude.Strings, Prelude.Chars,

99 Prelude.Functor, Prelude.Foldable,

10− Prelude.Traversable, Prelude.Bits, Prelude.Stream

10+ Prelude.Traversable, Prelude.Bits, Prelude.Stream,

11+

12+ Decidable.Equality

1113