Def Mathlib.Tactic.Translate.addTranslationFor

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.addTranslationForView on Github →
2026-10-04 05:36
Mathlib/Tactic/Translate/Core.lean
feat(Translate): implementation of `to_dual_for` command (#44270) …
Added Mathlib.Tactic.Translate.addTranslationForView on Github →