Def Mathlib.Tactic.Translate.warnParametricAttr

Modification history

2026-10-16 11:18
Mathlib/Tactic/Translate/Core.lean
refactor(Translate/Core): do not pass the `ref` around explicitly (#44835) …
Modified Mathlib.Tactic.Translate.warnParametricAttrView on Github →
2025-11-13 23:13
Mathlib/Tactic/ToAdditive/Frontend.lean
feat: `to_dual` attribute (#27887) …
Added Mathlib.Tactic.Translate.warnParametricAttrView on Github →