From bae4a5fc7cfeda57910f039d32b94505bc02bab2 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 3 Dec 2019 14:10:48 -0800 Subject: [PATCH] fix: use same approach used at `instantiateMVars` The idea is to beta reduce whenever we instantiate `?m` at `?m xs` with a lambda expression. --- src/Init/Lean/MetavarContext.lean | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/src/Init/Lean/MetavarContext.lean b/src/Init/Lean/MetavarContext.lean index 23c9deda51..296e6537ff 100644 --- a/src/Init/Lean/MetavarContext.lean +++ b/src/Init/Lean/MetavarContext.lean @@ -723,9 +723,13 @@ private partial def elimMVarDepsAux : Array Expr → Expr → M Expr | xs, e@(Expr.letE _ t v b _) => do t ← visit (elimMVarDepsAux xs) t; v ← visit (elimMVarDepsAux xs) v; b ← visit (elimMVarDepsAux xs) b; pure (e.updateLet! t v b) | xs, e@(Expr.mdata _ b _) => do b ← visit (elimMVarDepsAux xs) b; pure (e.updateMData! b) | xs, e@(Expr.app _ _ _) => e.withAppRev $ fun f revArgs => do + let wasMVar := f.isMVar; f ← visit (elimMVarDepsAux xs) f; revArgs ← revArgs.mapM (visit (elimMVarDepsAux xs)); - pure (mkAppRev f revArgs) + if wasMVar && f.isLambda then + pure (f.betaRev revArgs) + else + pure (mkAppRev f revArgs) | xs, e@(Expr.mvar mvarId _) => do mctx ← getMCtx; match mctx.getExprAssignment mvarId with