feat: make anonymous instance names not include proofs (#3934)

leanprover · Apr 17, 2024 · 319940d · 319940d
1 parent 11a9d2e
commit 319940d
Showing 1 changed file with 2 additions and 0 deletions.
diff --git a/src/Lean/Elab/DeclNameGen.lean b/src/Lean/Elab/DeclNameGen.lean
@@ -51,6 +51,8 @@ Expressions can also be replaced by `.bvar 0` if they shouldn't be mentioned.
 -/
 private partial def winnowExpr (e : Expr) : MetaM Expr := do
   let rec visit (e : Expr) : MonadCacheT Expr Expr MetaM Expr := checkCache e fun _ => do
+    if ← isProof e then
+      return .bvar 0
     match e with
     | .app .. =>
       if let some e' ← getParentProjArg e then