Def Mathlib.Tactic.Translate.insertTranslationChecked

Modification history

2026-09-04 15:28
Mathlib/Tactic/Translate/Core.lean
feat(Translate): try all translation pairings until one succeeds (#42861) …
Modified Mathlib.Tactic.Translate.insertTranslationCheckedView on Github →
2026-07-08 18:17
Mathlib/Tactic/Translate/Core.lean
feat(Translate): validate all translations (#40365) …
Added Mathlib.Tactic.Translate.insertTranslationCheckedView on Github →