0fca527 · Idris-dev · git.iko.soy

libs/base/Control/Isomorphism.idr−1

compare with master

unifiedsplit

@@ -1,7 +1,6 @@

1module Control.Isomorphism

2

3import Syntax.PreorderReasoning

4−import Uninhabited

5

4

6%default total

5%default total

7

6

libs/base/base.ipkg−2

@@ -10,8 +10,6 @@ modules = System,

10

11 Decidable.Decidable, Decidable.Order,

12

13− Uninhabited,

14−

15 Providers,

13 Providers,

16

14

17 Language.Reflection, Language.Reflection.Utils, Language.Reflection.Errors,

15 Language.Reflection, Language.Reflection.Utils, Language.Reflection.Errors,

libs/prelude/Prelude.idr+1

@@ -20,6 +20,7 @@ import Prelude.Chars

20import Prelude.Traversable

21import Prelude.Bits

22import Prelude.Stream

23+import Prelude.Uninhabited

23

24

24import Decidable.Equality

25import Decidable.Equality

25

26

libs/base/Uninhabited.idr → libs/prelude/Prelude/Uninhabited.idrrenamed+1−1

@@ -1,4 +1,4 @@

1−module Uninhabited

1+module Prelude.Uninhabited

2

3class Uninhabited t where

4 total uninhabited : t -> _|_

libs/prelude/prelude.ipkg+2−1

@@ -1,13 +1,14 @@

1package prelude

2

3opts = "--nobuiltins --total"

4−modules = Builtins, Prelude, IO,

4+modules = Builtins, Prelude, IO,

5

6 Prelude.Algebra, Prelude.Basics, Prelude.Bool, Prelude.Cast,

7 Prelude.Classes, Prelude.Nat, Prelude.Fin, Prelude.List,

8 Prelude.Maybe, Prelude.Monad, Prelude.Applicative, Prelude.Either,

9 Prelude.Vect, Prelude.Strings, Prelude.Chars, Prelude.Functor,

10 Prelude.Foldable, Prelude.Traversable, Prelude.Bits, Prelude.Stream,

11+ Prelude.Uninhabited,

11

12

12 Decidable.Equality

13 Decidable.Equality

13

14