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

fix: remove bad condition

Browse source 
Recall that `processAssignmentFOApprox` will unfold `v` if possible.
This commit is contained in:
Leonardo de Moura 2020-03-06 10:55:39 -08:00
parent 482e078b92
commit bce4912505
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

@ -616,7 +616,7 @@ private partial def processAssignmentAux (mvar : Expr) (mvarDecl : MetavarDecl)
else
pure false;
let useFOApprox : Unit → MetaM Bool := fun _ =>
if cfg.foApprox && v.isApp then
if cfg.foApprox then
condM (processAssignmentFOApprox mvar args v)
(pure true)
(useConstApprox ())