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

fix: pp.analyze restriction on _

Browse source
This commit is contained in:
Daniel Selsam 2021-07-31 07:37:08 -07:00 • committed by Sebastian Ullrich
parent 702211db2a
commit a84291641b
2 changed files with 10 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -321,10 +321,12 @@ partial def analyze (parentIsApp : Bool := false) : AnalyzeM Unit := do
| Expr.bvar .. => pure ()
where
analyzeApp := do
withKnowing true true $ analyzeAppStaged (← getExpr).getAppFn (← getExpr).getAppArgs
let couldBottomUp ← canBottomUp (← getExpr)
withReader (fun ctx => { ctx with inBottomUp := ctx.inBottomUp || (!ctx.knowsType && couldBottomUp) }) do
withKnowing true true $ analyzeAppStaged (← getExpr).getAppFn (← getExpr).getAppArgs
if !(← read).knowsType then
if !(← canBottomUp (← getExpr)) then
if !couldBottomUp then
annotateBool `pp.analysis.needsType
withType $ withKnowing true false $ analyze
else

6
tests/lean/run/PPTopDownAnalyze.lean
View file

@ -245,6 +245,12 @@ structure S2 where x : Unit
#testDelab (fun (u : Unit) => { x := () : S2 }) ()
expecting (fun (u : Unit) => { x := () : S2 }) ()
#testDelab Eq.refl True
expecting Eq.refl _
#testDelab (fun (u : Unit) => Eq.refl True) ()
expecting (fun (u : Unit) => Eq.refl True) ()
#testDelabN Nat.brecOn
#testDelabN Nat.below
#testDelabN Nat.mod_lt