Def Mathlib.Tactic.Reassoc.registerReassocExpr

Modification history

2026-10-06 10:22

Mathlib/Tactic/CategoryTheory/Reassoc.lean

chore: downgrade a few functions from IO to BaseIO (#44393) …

Modified Mathlib.Tactic.Reassoc.registerReassocExpr View on Github →

2026-01-21 16:04

Mathlib/Tactic/CategoryTheory/Reassoc.lean

feat(reassoc): tag the generated declaration with `to_dual none` (#33833) …

Added Mathlib.Tactic.Reassoc.registerReassocExpr View on Github →