Commit 2026-09-28 11:45 8438360d
View on Github →chore(Tactic/Translate): split long file (#44159)
This PR moves some material from Mathlib.Tactic.Translate.Core to a new file Mathlib.Tactic.Translate.Expr and to the existing Mathlib.Tactic.Translate.GuessName.
The new file now contains the implementation of expression translation. I removed the public section from it, instead marking the relevant definitions public.