Def Mathlib.Tactic.GuessName.renameBinderNames

Modification history

2026-09-28 11:45

Mathlib/Tactic/Translate/GuessName.lean

chore(Tactic/Translate): split long file (#44159) …

Added Mathlib.Tactic.GuessName.renameBinderNames View on Github →