# The `rename'` tactic #

The `rename'` tactic renames one or several hypotheses.

source
def Mathlib.Tactic.renameArg :
Lean.ParserDescr

A parser for a single rename to perform in the `rename` tactic: these should have the form `h => hnew` (describing a rename of a hypothesis `h` to `hnew`).

Equations

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

Instances For

source
def Mathlib.Tactic.rename' :
Lean.ParserDescr

`rename' h => hnew` renames the hypothesis named `h` to `hnew`. To rename several hypothesis, use `rename' h₁ => h₁new, h₂ => h₂new`. You can use `rename' a => b, b => a` to swap two variables.

Equations

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

Instances For