Def Mathlib.Tactic.registerGeneratingAttr

Modification history

2026-03-16 05:13

Mathlib/Tactic/Translate/Attributes.lean

feat(translate): support `to_additive (attr := to_fun)` (#36305) …

Added Mathlib.Tactic.registerGeneratingAttr View on Github →