From 126db5fb12565acd3f0da02fb657de9dd24ac71d Mon Sep 17 00:00:00 2001
From: Daniel Selsam <daniel.selsam@protonmail.com>
Date: Fri, 30 Jul 2021 11:36:55 -0700
Subject: [PATCH] fix: pp.analyze confirm def-eq before omitting arg

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

diff --git a/src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean b/src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean
index f8f22f5b24..eaa559472c 100644
--- a/src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean
+++ b/src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean
@@ -407,7 +407,8 @@ where
           match bInfos[i] with
           | BinderInfo.default =>
             if !(← valUnknown mvars[i]) && !(← read).inBottomUp && !(← isFunLike arg) then
-              annotateBool `pp.analysis.hole
+              if ← checkpointDefEq mvars[i] arg then
+                annotateBool `pp.analysis.hole
 
           | BinderInfo.implicit =>
             if (← valUnknown mvars[i] <||> higherOrders[i]) && !forceRegularApp then