Def Mathlib.Tactic.GuessName.GuessNameExt.addTranslation

Modification history

2026-05-09 23:47

Mathlib/Tactic/Translate/GuessName.lean

feat(Translate): locally modify name guessing dictionaries (#37808) …

Added Mathlib.Tactic.GuessName.GuessNameExt.addTranslation View on Github →