Def Mathlib.Tactic.UnfoldBoundary.UnfoldBoundaries.unfoldInsertions

Modification history

2026-02-12 13:23
Mathlib/Tactic/Translate/UnfoldBoundary.lean
perf(to_dual): first try translating without inserting casts (#35131) …
Deleted Mathlib.Tactic.UnfoldBoundary.UnfoldBoundaries.unfoldInsertionsView on Github →
2026-02-03 15:41
Mathlib/Tactic/Translate/UnfoldBoundary.lean
feat: unfold-boundaries in `to_dual` (#32438) …
Added Mathlib.Tactic.UnfoldBoundary.UnfoldBoundaries.unfoldInsertionsView on Github →