Lean4
/-- the `relevant_arg := ...` option tells which argument is a type where this declaration uses the
multiplicative structure. This is inferred automatically using the function `findMultiplicativeArg`,
but it can also be overwritten using this syntax.
If there are multiple arguments with a multiplicative structure, we typically tag the first one.
If this argument contains a fixed type, this declaration will not be additivized.
See the Heuristics section of the `to_additive` doc-string for more details.
If a declaration is not tagged, it is presumed that the first argument is relevant.
To indicate that there is no relevant argument, set it to a number that is out of bounds,
i.e. larger than the number of arguments, e.g. `(relevant_arg := 100)`.
Implementation note: we only allow exactly 1 relevant argument, even though some declarations
(like `Prod.instGroup`) have multiple arguments with a multiplicative structure on it.
The reason is that whether we additivize a declaration is an all-or-nothing decision, and
we will not be able to additivize declarations that (e.g.) talk about multiplication on `ℕ × α`
anyway.
-/
meta def toAdditiveRelevantOption : Lean.ParserDescr✝ :=
ParserDescr.nodeWithAntiquot✝ "toAdditiveRelevantOption" `ToAdditive.toAdditiveRelevantOption
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen ((with_annotate_term"&" @ParserDescr.nonReservedSymbol✝) "relevant_arg" false✝)
(ParserDescr.symbol✝ " := "))
(ParserDescr.const✝ `num))
