Def Mathlib.Tactic.Translate.findPrefixTranslation?

Modification history

2026-02-10 17:28

Mathlib/Tactic/Translate/Core.lean

refactor(translate): put `executeReservedNameAction` in a more natural place (#34999) …

Modified Mathlib.Tactic.Translate.findPrefixTranslation?View on Github →

2026-02-02 23:54

Mathlib/Tactic/Translate/Core.lean

perf(Tactic/Translate): merge some environment extensions (#34685) …

Added Mathlib.Tactic.Translate.findPrefixTranslation?View on Github →