Lean4
/-- An attribute that stores all the declarations that deal with numeric literals on variable types.
Numeral literals occur in expressions without type information, so in order to decide whether `1`
needs to be changed to `0`, the context around the numeral is relevant.
Most numerals will be in an `OfNat.ofNat` application, though tactics can add numeral literals
inside arbitrary functions. By default we assume that we do not change numerals, unless it is
in a function application with the `to_additive_change_numeral` attribute.
`@[to_additive_change_numeral n₁ ...]` should be added to all functions that take one or more
numerals as argument that should be changed if `additiveTest` succeeds on the first argument,
i.e. when the numeral is only translated if the first argument is a variable
(or consists of variables).
The arguments `n₁ ...` are the positions of the numeral arguments (starting counting from 1). -/
@[attr_parser 1000]
public meta def to_additive_change_numeral : Lean.ParserDescr✝ :=
ParserDescr.node✝ `ToAdditive.to_additive_change_numeral 1022
(ParserDescr.binary✝ `andthen (ParserDescr.nonReservedSymbol✝ "to_additive_change_numeral" false✝)
(ParserDescr.unary✝ `many (ParserDescr.binary✝ `andthen (ParserDescr.const✝ `ppSpace) (ParserDescr.const✝ `num))))
