From 7cdcb56c1d40a802c83a9e1c8d7971017e4b31cf Mon Sep 17 00:00:00 2001
From: Daniel Selsam <daniel.selsam@protonmail.com>
Date: Tue, 14 Sep 2021 12:31:23 -0700
Subject: [PATCH] feat: pp.analyze extend max heuristic to imax

---
 src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean b/src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean
index 80e1a04fb9..81d9b5493c 100644
--- a/src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean
+++ b/src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean
@@ -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