From d28419594e2a3c457708c74cedbdcc14a2e229d5 Mon Sep 17 00:00:00 2001 From: Daniel Selsam Date: Thu, 29 Jul 2021 15:36:18 -0700 Subject: [PATCH] fix: pp.analyze do not panic on bvar --- 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 a4621ce42f..10e6828547 100644 --- a/src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean +++ b/src/Lean/PrettyPrinter/Delaborator/TopDownAnalyze.lean @@ -318,7 +318,7 @@ partial def analyze (parentIsApp : Bool := false) : AnalyzeM Unit := do | Expr.letE .. => analyzeLet | Expr.lit .. => pure () | Expr.mvar .. => pure () - | Expr.bvar .. => unreachable! + | Expr.bvar .. => pure () where analyzeApp := do let needsType := !(← read).knowsType && !(← okBottomUp? (← getExpr)).isSafe