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

refactor: nested for-loop

Browse source
This commit is contained in:
Daniel Selsam 2021-07-31 14:00:49 -07:00 • committed by Sebastian Ullrich
parent 8dd8aea9c1
commit e55a5770f3
1 changed files with 6 additions and 12 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

18
src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean
View file

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