Def Mathlib.Tactic.Translate.insertTranslationsChecked

Modification history

2026-09-04 15:28

Mathlib/Tactic/Translate/Core.lean

feat(Translate): try all translation pairings until one succeeds (#42861) …

Added Mathlib.Tactic.Translate.insertTranslationsChecked View on Github →