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