Def Mathlib.Tactic.GuessName.registerGuessNameExt

Modification history

2026-05-09 23:47
Mathlib/Tactic/Translate/GuessName.lean
feat(Translate): locally modify name guessing dictionaries (#37808) …
Added Mathlib.Tactic.GuessName.registerGuessNameExtView on Github →