From e602bdc80c2e883e6b900f8111e0521e7dc490bc Mon Sep 17 00:00:00 2001 From: plp127 Date: Wed, 7 May 2025 02:53:13 -0400 Subject: [PATCH] fix: have `rename` ignore implementation detail hypotheses (#8241) This PR changes the behavior of the `rename` tactic to skip over implementation detail hypotheses when finding a hypothesis to rename. Closes #8240. --- src/Lean/Elab/Tactic/ElabTerm.lean | 2 +- tests/lean/run/renameSelf.lean | 11 +++++++++++ 2 files changed, 12 insertions(+), 1 deletion(-) create mode 100644 tests/lean/run/renameSelf.lean diff --git a/src/Lean/Elab/Tactic/ElabTerm.lean b/src/Lean/Elab/Tactic/ElabTerm.lean index a599dfc05b..440067e8c0 100644 --- a/src/Lean/Elab/Tactic/ElabTerm.lean +++ b/src/Lean/Elab/Tactic/ElabTerm.lean @@ -342,7 +342,7 @@ def elabAsFVar (stx : Syntax) (userName? : Option Name := none) : TacticM FVarId let fvarId ← withoutModifyingState <| withNewMCtxDepth <| withoutRecover do let type ← elabTerm typeStx none (mayPostpone := true) let fvarId? ← (← getLCtx).findDeclRevM? fun localDecl => do - if (← isDefEq type localDecl.type) then return localDecl.fvarId else return none + if !localDecl.isImplementationDetail && (← isDefEq type localDecl.type) then return localDecl.fvarId else return none match fvarId? with | none => throwError "failed to find a hypothesis with type{indentExpr type}" | some fvarId => return fvarId diff --git a/tests/lean/run/renameSelf.lean b/tests/lean/run/renameSelf.lean new file mode 100644 index 0000000000..47df6110af --- /dev/null +++ b/tests/lean/run/renameSelf.lean @@ -0,0 +1,11 @@ +variable {P Q : Prop} + +/-- +error: failed to find a hypothesis with type + P ↔ Q +-/ +#guard_msgs in +example : P ↔ Q := by + rename P ↔ Q => goal + obtain ⟨hpq, hqp⟩ := goal + constructor <;> trivial