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

feat: pp.analyze extend max heuristic to imax

Browse source
This commit is contained in:
Daniel Selsam 2021-09-14 12:31:23 -07:00 • committed by Sebastian Ullrich
parent 4646b36459
commit 7cdcb56c1d
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

@ -237,7 +237,7 @@ def mvarName (mvar : Expr) : MetaM Name := do
def containsBadMax : Level → Bool
| Level.succ u .. => containsBadMax u
| Level.max u v .. => (u.hasParam && v.hasParam) || containsBadMax u || containsBadMax v
| Level.imax u v .. => containsBadMax u || containsBadMax v
| Level.imax u v .. => (u.hasParam && v.hasParam) || containsBadMax u || containsBadMax v
| _ => false
open SubExpr