mathlib documentation

tactic.rename_var

Rename bound variable tactic

This files defines a tactic rename_var whose main purpose is to teach renaming of bound variables.

example (P :      Prop) (h :  n,  m, P n m) :  l,  m, P l m :=
begin
  rename_var n q at h, -- h is now ∀ (q : ℕ), ∃ (m : ℕ), P q m,
  rename_var m n, -- goal is now ∀ (l : ℕ), ∃ (n : ℕ), P k n,
  exact h -- Lean does not care about those bound variable names
end

Tags

teaching, tactic

meta def expr.rename_var  :
namenameexprexpr

Rename bound variable old to new in an expr

Rename bound variable old to new in goal

meta def tactic.rename_var_at_hyp  :
namenameexprtactic unit

Rename bound variable old to new in assumption h

rename_var old new renames all bound variables named old to new in the goal. rename_var old new at h does the same in hypothesis h.