Def Mathlib.Tactic.Translate.getRelevantArg

Modification history

2026-10-04 05:36
Mathlib/Tactic/Translate/Core.lean
feat(Translate): implementation of `to_dual_for` command (#44270) …
Modified Mathlib.Tactic.Translate.getRelevantArgView on Github →
2026-09-23 16:06
Mathlib/Tactic/Translate/Core.lean
feat(Translate): better `relevant_arg` heuristic (#43801) …
Modified Mathlib.Tactic.Translate.getRelevantArgView on Github →
2026-02-15 11:14
Mathlib/Tactic/Translate/Core.lean
feat(to_additive): automatically infer `relevant_arg` (#35318) …
Added Mathlib.Tactic.Translate.getRelevantArgView on Github →