Type definition from Decidable.Equality was moved to a separate module

This is done to make able for `Data.*` modules of datatypes declared in
prelude to import modules that have their own definitions of `DecEq`
inside them (i.e. modules of datatypes declared in the `base`).

libs/base/Decidable/Equality.idr

@@ -6,34 +6,10 @@ import Data.Nat
 import Data.List
 import Data.List1
 
+import public Decidable.Equality.Core as Decidable.Equality
+
 %default total
 
---------------------------------------------------------------------------------
--- Decidable equality
---------------------------------------------------------------------------------
-
-||| Decision procedures for propositional equality
-public export
-interface DecEq t where
-  ||| Decide whether two elements of `t` are propositionally equal
-  decEq : (x1 : t) -> (x2 : t) -> Dec (x1 = x2)
-
---------------------------------------------------------------------------------
--- Utility lemmas
---------------------------------------------------------------------------------
-
-||| The negation of equality is symmetric (follows from symmetry of equality)
-export
-negEqSym : forall a, b . (a = b -> Void) -> (b = a -> Void)
-negEqSym p h = p (sym h)
-
-||| Everything is decidably equal to itself
-export
-decEqSelfIsYes : DecEq a => {x : a} -> decEq x x = Yes Refl
-decEqSelfIsYes {x} with (decEq x x)
-  decEqSelfIsYes {x} | Yes Refl = Refl
-  decEqSelfIsYes {x} | No contra = absurd $ contra Refl
-
 --------------------------------------------------------------------------------
 --- Unit
 --------------------------------------------------------------------------------

libs/base/Decidable/Equality/Core.idr

@@ -0,0 +1,29 @@
+module Decidable.Equality.Core
+
+%default total
+
+--------------------------------------------------------------------------------
+-- Decidable equality
+--------------------------------------------------------------------------------
+
+||| Decision procedures for propositional equality
+public export
+interface DecEq t where
+  ||| Decide whether two elements of `t` are propositionally equal
+  decEq : (x1 : t) -> (x2 : t) -> Dec (x1 = x2)
+
+--------------------------------------------------------------------------------
+-- Utility lemmas
+--------------------------------------------------------------------------------
+
+||| The negation of equality is symmetric (follows from symmetry of equality)
+export
+negEqSym : forall a, b . (a = b -> Void) -> (b = a -> Void)
+negEqSym p h = p (sym h)
+
+||| Everything is decidably equal to itself
+export
+decEqSelfIsYes : DecEq a => {x : a} -> decEq x x = Yes Refl
+decEqSelfIsYes {x} with (decEq x x)
+  decEqSelfIsYes {x} | Yes Refl = Refl
+  decEqSelfIsYes {x} | No contra = absurd $ contra Refl

libs/base/base.ipkg

@@ -49,6 +49,7 @@ modules = Control.App,
 
           Decidable.Decidable,
           Decidable.Equality,
+          Decidable.Equality.Core,
           Decidable.Order,
 
           Language.Reflection,