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

fix: only pp.analyze when all is not set

Browse source
This commit is contained in:
Daniel Selsam 2021-07-30 11:37:21 -07:00 • committed by Sebastian Ullrich
parent 126db5fb12
commit 1f183cdc30
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/Basic.lean
View file

@ -391,7 +391,7 @@ def delab (currNamespace : Name) (openDecls : List OpenDecl) (e : Expr) (options
catch _ => pure ()
let e ← if getPPInstantiateMVars opts then ← Meta.instantiateMVars e else e
let optionsPerPos ←
if getPPAnalyze opts && optionsPerPos.isEmpty then
if !getPPAll opts && getPPAnalyze opts && optionsPerPos.isEmpty then
topDownAnalyze e
else optionsPerPos
catchInternalId Delaborator.delabFailureId