Documentation

Mathlib.Tactic.RenameBVar

Renames a bound variable in a hypothesis.

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

    Renames a bound variable in the target.

    Equations
    Instances For
      • 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 :=
      begin
        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
      end
      

      Note: name clashes are resolved automatically.

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