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

fix: pp.analyze skip all omitted instances

Browse source
This commit is contained in:
Daniel Selsam 2021-09-14 16:13:36 -07:00 • committed by Sebastian Ullrich
parent 5eed3b73bf
commit a35cbb5844
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/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean
View file

@ -600,7 +600,7 @@ mutual
if ← checkpointDefEq inst arg then annotateBool `pp.analysis.skip; provided := false
else annotateNamedArg (← mvarName mvars[i])
| _ => annotateNamedArg (← mvarName mvars[i])
else provided := false
else annotateBool `pp.analysis.skip; provided := false
modify fun s => { s with provideds := s.provideds.set! i provided }
| BinderInfo.auxDecl => pure ()
if (← get).provideds[i] then withKnowing (not (← typeUnknown mvars[i])) true analyze