From 482e078b92e9af05183cc191180bb20235ed77d9 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 6 Mar 2020 10:46:48 -0800 Subject: [PATCH] chore: minor cleanup --- src/Init/Lean/Meta/ExprDefEq.lean | 11 +++++------ 1 file changed, 5 insertions(+), 6 deletions(-) diff --git a/src/Init/Lean/Meta/ExprDefEq.lean b/src/Init/Lean/Meta/ExprDefEq.lean index 0fe89b6edd..4991c45992 100644 --- a/src/Init/Lean/Meta/ExprDefEq.lean +++ b/src/Init/Lean/Meta/ExprDefEq.lean @@ -603,10 +603,10 @@ match v? with v ← mkLambda xs v; checkTypesAndAssign mvar v -private partial def processAssignmentAux (mvar : Expr) (mvarDecl : MetavarDecl) (v : Expr) : Nat → Array Expr → MetaM Bool -| i, args => +private partial def processAssignmentAux (mvar : Expr) (mvarDecl : MetavarDecl) : Nat → Array Expr → Expr → MetaM Bool +| i, args, v => do + cfg ← getConfig; if h : i < args.size then do - cfg ← getConfig; let arg := args.get ⟨i, h⟩; arg ← simpAssignmentArg arg; let args := args.set ⟨i, h⟩ arg; @@ -629,11 +629,10 @@ private partial def processAssignmentAux (mvar : Expr) (mvarDecl : MetavarDecl) else if mvarDecl.lctx.contains fvarId && !cfg.quasiPatternApprox then useFOApprox () else - processAssignmentAux (i+1) args + processAssignmentAux (i+1) args v | _ => useFOApprox () else do - cfg ← getConfig; v ← instantiateMVars v; -- enforce A4 if cfg.foApprox && !args.isEmpty && v.getAppFn == mvar then -- using A6 @@ -668,7 +667,7 @@ traceCtx `Meta.isDefEq.assign $ do trace! `Meta.isDefEq.assign (mvarApp ++ " := " ++ v); let mvar := mvarApp.getAppFn; mvarDecl ← getMVarDecl mvar.mvarId!; - processAssignmentAux mvar mvarDecl v 0 mvarApp.getAppArgs + processAssignmentAux mvar mvarDecl 0 mvarApp.getAppArgs v private def isDeltaCandidate (t : Expr) : MetaM (Option ConstantInfo) := match t.getAppFn with