rename'

Mathlib.Tactic.Rename

URI: https://scilib.ai/kg/mathlib#Mathlib.Tactic.rename'

Lean4

/-- `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. -/
@[tactic_parser 1000]
public meta def rename' : Lean.ParserDescr✝ :=
  ParserDescr.node✝ `Mathlib.Tactic.rename' 1022
    (ParserDescr.binary✝ `andthen (ParserDescr.nonReservedSymbol✝ "rename' " false✝)
      ((with_annotate_term"sepBy1(" @ParserDescr.sepBy1✝) Mathlib.Tactic.renameArg "," (ParserDescr.symbol✝ ", ")
        Bool.false✝))

Похожие утверждения

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru