Def Mathlib.Tactic.Translate.ensureClassTranslated

Modification history

2026-09-23 16:06
Mathlib/Tactic/Translate/Core.lean
feat(Translate): better `relevant_arg` heuristic (#43801) …
Added Mathlib.Tactic.Translate.ensureClassTranslatedView on Github →