addRelatedDecl

def Mathlib.Tactic.addRelatedDecl (src : Lean.Name) (suffix : String) (ref : Lean.Syntax) (attrs? : Option (Lean.Syntax.TSepArray `Lean.Parser.Term.attrInstance ",")) (construct : Lean.Expr → Lean.Expr → List Lean.Name → Lean.MetaM (Lean.Expr × List Lean.Name)) : Lean.MetaM Unit

A helper function for constructing a related declaration from an existing one.

This is currently used by the attributes reassoc and elementwise, and has been factored out to avoid code duplication. Feel free to add features as needed for other applications.

This helper:

• calls addDeclarationRangesFromSyntax, so jump-to-definition works,
• copies the protected status of the existing declaration, and
• supports copying attributes.

Arguments:

• src : Name is the existing declaration that we are modifying.
• suffix : String will be appended to src to form the name of the new declaration.
• ref : Syntax is the syntax where the user requested the related declaration.
• construct type value levels : MetaM (Expr × List Name) given the type, value, and universe variables of the original declaration, should construct the value of the new declaration, along with the names of its universe variables.
• attrs is the attributes that should be applied to both the new and the original declaration, e.g. in the usage @[reassoc (attr := simp)]. We apply it to both declarations, to have the same behavior as to_additive, and to shorten some attribute commands. Note that @[elementwise (attr := simp), reassoc (attr := simp)] will try to apply simp twice to the current declaration, but that causes no issues.