From e55a5770f313681e7a6cefd13c16f82de714ac37 Mon Sep 17 00:00:00 2001 From: Daniel Selsam Date: Sat, 31 Jul 2021 14:00:49 -0700 Subject: [PATCH] refactor: nested for-loop --- .../Delaborator/TopDownAnalyze.lean | 18 ++++++------------ 1 file changed, 6 insertions(+), 12 deletions(-) diff --git a/src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean b/src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean index d900c01b75..143c72cf7e 100644 --- a/src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean +++ b/src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean @@ -370,18 +370,12 @@ where -- Collect explicit arguments that can be elaborated without expected type, with *no* top-down info -- Note: we perform this before the next pass because we prefer simple bottom-ups to unify first before -- more complex ones. - for i in [:args.size] do - if bInfos[i] == BinderInfo.default then - if ← valUnknown mvars[i] <&&> canBottomUp args[i] then - tryUnify args[i] mvars[i] - bottomUps := bottomUps.set! i true - - -- Now, collect explicit arguments that can be elaborated with *incomplete* top-down info - for i in [:args.size] do - if !bottomUps[i] && bInfos[i] == BinderInfo.default then - if ← valUnknown mvars[i] <&&> canBottomUp args[i] mvars[i] then - tryUnify args[i] mvars[i] - bottomUps := bottomUps.set! i true + for target in [fun _ => none, fun i => some mvars[i]] do + for i in [:args.size] do + if bInfos[i] == BinderInfo.default then + if ← valUnknown mvars[i] <&&> canBottomUp args[i] (target i) then + tryUnify args[i] mvars[i] + bottomUps := bottomUps.set! i true -- Next, look at out params for i in [:args.size] do