diff options
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 |