made constructor for DecEq available

stefan-hoeck · Nov 26, 2020 · 527a5b5 · 527a5b5
1 parent f4e2dff
commit 527a5b5
Showing 1 changed file with 7 additions and 0 deletions.
diff --git a/src/Language/Reflection/Derive.idr b/src/Language/Reflection/Derive.idr
@@ -5,6 +5,7 @@
 ||| using the functionality provided here.
 module Language.Reflection.Derive
 
+import Decidable.Equality
 import public Language.Reflection.Syntax
 import public Language.Reflection.Types
 
@@ -326,3 +327,9 @@ mkMonoid' = %runElab check (var $ singleCon "Monoid")
 public export %inline
 mkMonoid : (1 semi : Semigroup a) => (neutral : a) -> Monoid a
 mkMonoid = mkMonoid' semi
+
+||| Creates a `DecEq` value from the passed implementation function
+||| for `decEq`
+public export %inline
+mkDecEq : (decEq : (x1 : a) -> (x2 : a) -> Dec (x1 = x2)) -> DecEq a
+mkDecEq = %runElab check (var $ singleCon "DecEq")