From 5a994ac0e224d72851c26119b79a58521df1732c Mon Sep 17 00:00:00 2001
From: rhiannon morris <rhi@rhiannon.website>
Date: Sat, 25 Mar 2023 20:49:14 +0100
Subject: [PATCH] derive Eq,Ord,Show for DimEq

---
 lib/Quox/Syntax/DimEq.idr | 4 +++-
 tests/TypingImpls.idr     | 2 --
 2 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/lib/Quox/Syntax/DimEq.idr b/lib/Quox/Syntax/DimEq.idr
index 39a2383..6595167 100644
--- a/lib/Quox/Syntax/DimEq.idr
+++ b/lib/Quox/Syntax/DimEq.idr
@@ -11,7 +11,9 @@ import Data.DPair
 import Data.Fun.Graph
 import Decidable.Decidable
 import Decidable.Equality
+import Derive.Prelude
 
+%language ElabReflection
 %default total
 
 
@@ -24,8 +26,8 @@ public export
 data DimEq : Nat -> Type where
   ZeroIsOne : DimEq d
   C         : (eqs : DimEq' d) -> DimEq d
-
 %name DimEq eqs
+%runElab deriveIndexed "DimEq" [Eq, Ord, Show]
 
 
 public export
diff --git a/tests/TypingImpls.idr b/tests/TypingImpls.idr
index c1a0517..41044fa 100644
--- a/tests/TypingImpls.idr
+++ b/tests/TypingImpls.idr
@@ -11,8 +11,6 @@ import Derive.Prelude
 
 %runElab derive "Reduce.WhnfError" [Show]
 
-%runElab deriveIndexed "DimEq" [Show]
-
 export %hint
 showTyContext : (IsQty q, PrettyHL q, Show q) => Show (TyContext q d n)
 showTyContext = deriveShow