Lean4
/-- * `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`.
```lean
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.
-/
@[tactic_parser 1000]
public meta def «tacticRename_bvar_→__» : Lean.ParserDescr✝ :=
ParserDescr.node✝ `Mathlib.Tactic.«tacticRename_bvar_→__» 1022
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen (ParserDescr.nonReservedSymbol✝ "rename_bvar " false✝)
(ParserDescr.const✝ `ident))
(ParserDescr.symbol✝ " → "))
(ParserDescr.const✝ `ident))
(ParserDescr.unary✝ `optional Lean.Parser.Tactic.location))
