The rename_bvar tactic

This file defines the rename_bvar tactic, for renaming bound variables.

def Mathlib.Tactic.renameBVarHyp (mvarId : Lean.MVarId) (fvarId : Lean.FVarId) (old new : Lean.Name) : Lean.MetaM Unit

Renames a bound variable in a hypothesis.

Equations

• Mathlib.Tactic.renameBVarHyp mvarId fvarId old new = Mathlib.Tactic.modifyLocalDecl mvarId fvarId fun (ldecl : Lean.LocalDecl) => ldecl.setType (ldecl.type.renameBVar old new)

def Mathlib.Tactic.renameBVarTarget (mvarId : Lean.MVarId) (old new : Lean.Name) : Lean.MetaM Unit

Renames a bound variable in the target.

Equations

• Mathlib.Tactic.renameBVarTarget mvarId old new = Mathlib.Tactic.modifyTarget mvarId fun (e : Lean.Expr) => e.renameBVar old new

def Mathlib.Tactic.«tacticRename_bvar_→__» : Lean.ParserDescr

• rename_bvar old → new renames all bound variables named old to new in the target.
• rename_bvar old → new at h does the same in hypothesis h.

example (P : ℕ → ℕ → Prop) (h : ∀ n, ∃ m, P n m) : ∀ l, ∃ m, P l m := by
  rename_bvar n → q at h -- h is now ∀ (q : ℕ), ∃ (m : ℕ), P q m,
  rename_bvar m → n -- target is now ∀ (l : ℕ), ∃ (n : ℕ), P k n,
  exact h -- Lean does not care about those bound variable names

Note: name clashes are resolved automatically.

Equations

• One or more equations did not get rendered due to their size.