Def Mathlib.Tactic.Translate.updateAndAddDecl

Modification history

2026-02-12 13:23

Mathlib/Tactic/Translate/Core.lean

perf(to_dual): first try translating without inserting casts (#35131) …

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