Def Mathlib.Tactic.Translate.proceedFieldsAux

Modification history

2026-02-15 11:14
Mathlib/Tactic/Translate/Core.lean
feat(to_additive): automatically infer `relevant_arg` (#35318) …
Modified Mathlib.Tactic.Translate.proceedFieldsAuxView on Github →
2026-02-02 23:54
Mathlib/Tactic/Translate/Core.lean
perf(Tactic/Translate): merge some environment extensions (#34685) …
Modified Mathlib.Tactic.Translate.proceedFieldsAuxView on Github →
2026-01-12 23:59
Mathlib/Tactic/Translate/Core.lean
feat(translate): linter for overwriting existing translations (#33777) …
Modified Mathlib.Tactic.Translate.proceedFieldsAuxView on Github →
2025-11-13 23:13
Mathlib/Tactic/ToAdditive/Frontend.lean
feat: `to_dual` attribute (#27887) …
Added Mathlib.Tactic.Translate.proceedFieldsAuxView on Github →