to_additive_ignore_args — Mathlib

Lean4

/-- An attribute that tells `@[to_additive]` that certain arguments of this definition are not
involved when using `@[to_additive]`.
This helps the heuristic of `@[to_additive]` by also transforming definitions if `ℕ` or another
fixed type occurs as one of these arguments. -/
@[attr_parser 1000]
public meta def to_additive_ignore_args : Lean.ParserDescr✝ :=
  ParserDescr.node✝ `ToAdditive.to_additive_ignore_args 1022
    (ParserDescr.binary✝ `andthen (ParserDescr.nonReservedSymbol✝ "to_additive_ignore_args" false✝)
      (ParserDescr.unary✝ `many (ParserDescr.binary✝ `andthen (ParserDescr.const✝ `ppSpace) (ParserDescr.const✝ `num))))

Похожие утверждения