Browse Source

Remove special handling of neutral I-eliminations in unifier

master
Amélia Liao 3 years ago
parent
commit
8937bc16cc
1 changed files with 0 additions and 16 deletions
  1. +0
    -16
      src/Elab/Eval.hs

+ 0
- 16
src/Elab/Eval.hs View File

@ -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)


Loading…
Cancel
Save