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

libs/base/base.ipkg+1−1

compare with master

unifiedsplit

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

8

9 System.Concurrency.Raw, System.Concurrency.Process,

10

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

11+ Decidable.Decidable, Decidable.Order,

12

13 Uninhabited,

14

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

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

1module Decidable.Equality

2

3+import Builtins

4+import Prelude.Either

5+import Prelude.List

6+import Prelude.Vect

3−import Prelude

7+import Prelude.Fin

8+import Prelude.Maybe

4

9

5--------------------------------------------------------------------------------

10--------------------------------------------------------------------------------

6-- Utility lemmas

11-- Utility lemmas

libs/prelude/Prelude.idr+2

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

19import Prelude.Bits

20import Prelude.Stream

21

22+import Decidable.Equality

23+

22%access public

24%access public

23%default total

25%default total

24

26

libs/prelude/prelude.ipkg+3−1

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

7 Prelude.List, Prelude.Maybe, Prelude.Monad, Prelude.Applicative,

8 Prelude.Either, Prelude.Vect, Prelude.Strings, Prelude.Chars,

9 Prelude.Functor, Prelude.Foldable,

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

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

11+

12+ Decidable.Equality

11

13