Commit 2026-03-14 12:09 cd059f10

View on Github →

feat(Translate): add support for specifying argument names (#36402) This PR adds a (rename := x → y, ...) option to @[to_additive] and @[to_dual] for specifying the argument names of the translated declaration.

Estimated changes

Modified Mathlib/Order/Hom/Lattice.lean

deleted theorem InfHom.mk_le_mk

deleted def InfHom.subtypeVal

deleted theorem InfHom.subtypeVal_apply

deleted theorem InfHom.subtypeVal_coe

modified theorem SupHom.mk_le_mk

Modified Mathlib/Order/Lattice.lean

Modified Mathlib/Tactic/Translate/Core.lean

added def Mathlib.Tactic.Translate.elabRename

modified def Mathlib.Tactic.Translate.renameBinderNames

Modified Mathlib/Tactic/Translate/ToAdditive.lean

Modified Mathlib/Tactic/Translate/ToDual.lean

Modified MathlibTest/ToDual.lean

added def renameTest