max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix: missing !

Browse source
This commit is contained in:
Leonardo de Moura 2019-12-19 10:27:49 -08:00
parent bdc9ea6fc6
commit 40576ac3dd
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Init/Lean/Meta/ExprDefEq.lean
View file

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