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

fix: pp.analyze was still printing inaccessibles

Browse source
This commit is contained in:
Daniel Selsam 2021-07-29 11:35:15 -07:00 • committed by Sebastian Ullrich
parent 912e5cf212
commit d6412b3a98
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

@ -360,7 +360,7 @@ where
match instResult with
| LOption.some inst =>
if ← checkpointDefEq inst arg then annotateBool `pp.analysis.skip
else annotateBool `pp.analysis.namedArg
else discard <| annotateNamedArg (← mvarName mvars[i]) appPos
| _ => discard <| annotateNamedArg (← mvarName mvars[i]) appPos
| BinderInfo.auxDecl => pure ()
| BinderInfo.strictImplicit => unreachable!