diff options
| author | Tom Smeding <tom@tomsmeding.com> | 2026-05-25 14:08:07 +0200 |
|---|---|---|
| committer | Tom Smeding <tom@tomsmeding.com> | 2026-05-25 14:08:07 +0200 |
| commit | ac13ffebefb22ec45e29e7f4bb6d53fa46cf6475 (patch) | |
| tree | a4edfb35804ce46dcf683c35b5988cb003afb218 /src/CHAD/AST/Weaken.hs | |
| parent | f5b1b405fa4ba63bdffe0f2998f655f0b06534bf (diff) | |
Diffstat (limited to 'src/CHAD/AST/Weaken.hs')
| -rw-r--r-- | src/CHAD/AST/Weaken.hs | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/src/CHAD/AST/Weaken.hs b/src/CHAD/AST/Weaken.hs index ac0d152..f5345d1 100644 --- a/src/CHAD/AST/Weaken.hs +++ b/src/CHAD/AST/Weaken.hs @@ -37,6 +37,9 @@ instance GEq (Idx env) where geq (IS i) (IS j) | Just Refl <- geq i j = Just Refl geq _ _ = Nothing +instance Eq (Idx env t) where _ == _ = True +instance EqP (Idx env) where eqp = eqpFromGEq + splitIdx :: forall env2 env1 t f. SList f env1 -> Idx (Append env1 env2) t -> Either (Idx env1 t) (Idx env2 t) splitIdx SNil i = Right i splitIdx (SCons _ _) IZ = Left IZ |