toAdditiveRest — Mathlib

Lean4
/-- Remaining arguments of `to_additive`. -/
meta def toAdditiveRest : Lean.ParserDescr✝ :=
  ParserDescr.nodeWithAntiquot✝ "toAdditiveRest" `ToAdditive.toAdditiveRest
    (ParserDescr.binary✝ `andthen
      (ParserDescr.binary✝ `andthen
        (ParserDescr.binary✝ `andthen ToAdditive.toAdditiveNameHint
          (ParserDescr.unary✝ `many
            (ParserDescr.binary✝ `andthen (ParserDescr.const✝ `ppSpace) ToAdditive.toAdditiveOption)))
        (ParserDescr.unary✝ `optional
          (ParserDescr.binary✝ `andthen (ParserDescr.const✝ `ppSpace) (ParserDescr.const✝ `ident))))
      (ParserDescr.unary✝ `optional
        (ParserDescr.binary✝ `andthen (ParserDescr.const✝ `ppSpace)
          (ParserDescr.binary✝ `orelse (ParserDescr.const✝ `str) (ParserDescr.const✝ `docComment)))))
Похожие утверждения