Def Mathlib.Tactic.Translate.elabRename

Modification history

2026-03-14 12:09
Mathlib/Tactic/Translate/Core.lean
feat(Translate): add support for specifying argument names (#36402) …
Added Mathlib.Tactic.Translate.elabRenameView on Github →