rhi/quox
rhi/quox
1
0
Fork 0
Code Issues 15 Pull requests 1 Releases Wiki Activity

derive Eq,Ord,Show for DimEq

Browse source
This commit is contained in:
rhiannon morris 2023-03-25 20:49:14 +01:00
parent ab82883214
commit 5a994ac0e2
2 changed files with 3 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
lib/Quox/Syntax/DimEq.idr
View file

@ -11,7 +11,9 @@ import Data.DPair
import Data.Fun.Graph import Data.Fun.Graph
import Decidable.Decidable import Decidable.Decidable
import Decidable.Equality import Decidable.Equality
import Derive.Prelude
%language ElabReflection
%default total %default total
@ -24,8 +26,8 @@ public export
data DimEq : Nat -> Type where data DimEq : Nat -> Type where
ZeroIsOne : DimEq d ZeroIsOne : DimEq d
C : (eqs : DimEq' d) -> DimEq d C : (eqs : DimEq' d) -> DimEq d
%name DimEq eqs %name DimEq eqs
%runElab deriveIndexed "DimEq" [Eq, Ord, Show]
public export public export

2
tests/TypingImpls.idr
View file

@ -11,8 +11,6 @@ import Derive.Prelude
%runElab derive "Reduce.WhnfError" [Show] %runElab derive "Reduce.WhnfError" [Show]
%runElab deriveIndexed "DimEq" [Show]
export %hint export %hint
showTyContext : (IsQty q, PrettyHL q, Show q) => Show (TyContext q d n) showTyContext : (IsQty q, PrettyHL q, Show q) => Show (TyContext q d n)
showTyContext = deriveShow showTyContext = deriveShow