From 40576ac3dd3d5020c1e652b06b10e670f850ef9b Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 19 Dec 2019 10:27:49 -0800 Subject: [PATCH] fix: missing `!` --- src/Init/Lean/Meta/ExprDefEq.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Init/Lean/Meta/ExprDefEq.lean b/src/Init/Lean/Meta/ExprDefEq.lean index 4375b3baf7..b9c7c9a294 100644 --- a/src/Init/Lean/Meta/ExprDefEq.lean +++ b/src/Init/Lean/Meta/ExprDefEq.lean @@ -678,7 +678,7 @@ private partial def processAssignmentAux (mvar : Expr) (mvarDecl : MetavarDecl) else do cfg ← getConfig; v ← instantiateMVars v; -- enforce A4 - if cfg.foApprox && args.isEmpty && v.getAppFn == mvar then + if cfg.foApprox && !args.isEmpty && v.getAppFn == mvar then -- using A6 processAssignmentFOApprox mvar args v else do