Def Mathlib.Tactic.Translate.elabArgStx

Modification history

2025-11-19 10:28

Mathlib/Tactic/Translate/Core.lean

feat(to_additive): allow referring to arguments by name (#31748) …

Added Mathlib.Tactic.Translate.elabArgStx View on Github →