Def Mathlib.Tactic.Translate.getRelevantArg

Modification history

2026-02-15 11:14

Mathlib/Tactic/Translate/Core.lean

feat(to_additive): automatically infer `relevant_arg` (#35318) …

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