Documentation

Mathlib.Tactic.Rename

The rename' tactic #

The rename' tactic renames one or several hypotheses.

source
🔸 coverage
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).

Instances For
    source
    🔸 coverage
    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.

    Instances For