Combining attributes that generate declarations with translation attributes

This file defines extensible support for writing e.g. to_additive (attr := simps) such that all of the declarations generated by simps will pairwise be added to the to_additive dictictionary.

opaque Mathlib.Tactic.generatingAttrs : IO.Ref (Lean.NameMap (Lean.Name → Lean.Syntax → Lean.AttributeKind → Lean.AttrM (Array Lean.Name)))

Attributes that generate new declarations when applied.

def Mathlib.Tactic.registerGeneratingAttr (attr : Lean.Name) (impl : Lean.Name → Lean.Syntax → Lean.AttributeKind → Lean.AttrM (Array Lean.Name)) : IO Unit

For an attribute that generates new declarations, register the implementation that returns the generated declarations. This will be used by translation attributes for translating between generated declarations.

Equations

• One or more equations did not get rendered due to their size.