fix: pp.analyze confirm def-eq before omitting arg

2021-07-30 11:36:55 -07:00 · 2021-07-30 11:36:55 -07:00 · 126db5fb12
commit 126db5fb12
parent 3bef119136
1 changed files with 2 additions and 1 deletions
--- 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