Lean4
/-- `reorder := ...` reorders the arguments/hypotheses in the generated declaration.
It uses cycle notation. For example `(reorder := 1 2, 5 6)` swaps the first two
arguments with each other and the fifth and the sixth argument and `(reorder := 3 4 5)` will move
the fifth argument before the third argument. This is used in `to_dual` to swap the arguments in
`≤`, `<` and `⟶`. It is also used in `to_additive` to translate from `^` to `•`.
-/
meta def toAdditiveReorderOption : Lean.ParserDescr✝ :=
ParserDescr.nodeWithAntiquot✝ "toAdditiveReorderOption" `ToAdditive.toAdditiveReorderOption
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen ((with_annotate_term"&" @ParserDescr.nonReservedSymbol✝) "reorder" false✝)
(ParserDescr.symbol✝ " := "))
((with_annotate_term"sepBy1(" @ParserDescr.sepBy1✝) (ParserDescr.unary✝ `many1 (ParserDescr.const✝ `num)) ","
(ParserDescr.symbol✝ ", ") Bool.false✝))
