Def Mathlib.Tactic.Translate.renameBinderNames

Modification history

2026-05-09 23:47
Mathlib/Tactic/Translate/Core.lean
feat(Translate): locally modify name guessing dictionaries (#37808) …
Modified Mathlib.Tactic.Translate.renameBinderNamesView on Github →
2026-03-20 01:59
Mathlib/Tactic/Translate/Core.lean
feat(Translate): translate binder names starting with `h` (#36304) …
Modified Mathlib.Tactic.Translate.renameBinderNamesView on Github →
2026-03-14 12:09
Mathlib/Tactic/Translate/Core.lean
feat(Translate): add support for specifying argument names (#36402) …
Modified Mathlib.Tactic.Translate.renameBinderNamesView on Github →
2025-11-13 23:13
Mathlib/Tactic/ToAdditive/Frontend.lean
feat: `to_dual` attribute (#27887) …
Added Mathlib.Tactic.Translate.renameBinderNamesView on Github →