fix: ignore implementationDetail hyps in rename_i (#5183)

Closes #5176
leanprover · Aug 27, 2024 · 4436638 · 4436638
1 parent 095c7b2
commit 4436638
Show file tree

Hide file tree

Showing 2 changed files with 16 additions and 0 deletions.
diff --git a/src/Lean/Elab/Tactic/BuiltinTactic.lean b/src/Lean/Elab/Tactic/BuiltinTactic.lean
@@ -458,6 +458,8 @@ def renameInaccessibles (mvarId : MVarId) (hs : TSyntaxArray ``binderIdent) : Ta
       match lctx.getAt? j with
       | none => pure ()
       | some localDecl =>
+        if localDecl.isImplementationDetail then
+          continue
         let inaccessible := !(extractMacroScopes localDecl.userName |>.equalScope callerScopes)
         let shadowed := found.contains localDecl.userName
         if inaccessible || shadowed then

diff --git a/tests/lean/run/5176.lean b/tests/lean/run/5176.lean
@@ -0,0 +1,14 @@
+class Foo where
+
+class Bar extends Foo where
+  bar : True
+
+def foo : Foo := {}
+
+example [Bar] : Bar := {
+  foo with bar := by {
+    rename_i inst
+    guard_hyp inst : Bar
+    trivial
+  }
+}