From 27e9be176fbaa66a28011408df228e7ff2bdee7d Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Abigail=20Magalh=C3=A3es?= Date: Mon, 1 Mar 2021 09:50:31 -0300 Subject: [PATCH] Remove special handling of neutral I-eliminations in unifier --- src/Elab/Eval.hs | 16 ---------------- 1 file changed, 16 deletions(-) diff --git a/src/Elab/Eval.hs b/src/Elab/Eval.hs index 02901c9..bda55f5 100644 --- a/src/Elab/Eval.hs +++ b/src/Elab/Eval.hs @@ -234,22 +234,6 @@ unify' topa topb = join $ go <$> forceIO topa <*> forceIO topb where | x == x', length a == length a' = traverse_ (uncurry unify'Spine) (Seq.zip a a') - go lhs@(VNe _hd (_ Seq.:|> PIElim _l x y i)) rhs = - case force i of - VI0 -> unify' x rhs - VI1 -> unify' y rhs - _ -> case rhs of - VSystem sys -> goSystem (flip unify') sys lhs - _ -> fail - - go lhs rhs@(VNe _hd (_ Seq.:|> PIElim _l x y i)) = - case force i of - VI0 -> unify' lhs x - VI1 -> unify' lhs y - _ -> case lhs of - VSystem sys -> goSystem unify' sys rhs - _ -> fail - go (VLam p (Closure _ k)) vl = do t <- VVar <$> newName unify' (k t) (vApp p vl t)