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.

Estimated changes