Lean4
/-- Warn the user when the multiplicative declaration has an attribute. -/
def warnAttrCore (stx : Syntax) (f : Environment → Name → Bool) (thisAttr attrName src tgt : Name) : CoreM Unit := do
if f (← getEnv) src then
Linter.logLintIf linter.existingAttributeWarning stx <|
(m! "The source declaration {src } was given attribute {attrName } before calling @[{thisAttr }]. \
The preferred method is to use `@[{thisAttr } (attr := {attrName })]` to apply the \
attribute to both {src } and the target declaration {tgt}.") ++
if thisAttr == `to_additive then
m! "\nSpecial case: If this declaration was generated by @[to_additive] \
itself, you can use @[to_additive (attr := to_additive, {attrName})] on the original \
declaration."
else ""
