toAdditiveNameHint — Mathlib

Lean4
/-- An `existing` or `self` name hint for `to_additive`. -/
meta def toAdditiveNameHint : Lean.ParserDescr✝ :=
  ParserDescr.nodeWithAntiquot✝ "toAdditiveNameHint" `ToAdditive.toAdditiveNameHint
    (ParserDescr.unary✝ `optional
      (ParserDescr.binary✝ `andthen (ParserDescr.const✝ `ppSpace)
        (ParserDescr.binary✝ `orelse
          (ParserDescr.nodeWithAntiquot✝ "existing" `token.existing
            ((with_annotate_term"&" @ParserDescr.nonReservedSymbol✝) "existing" false✝))
          (ParserDescr.nodeWithAntiquot✝ "self" `token.self
            ((with_annotate_term"&" @ParserDescr.nonReservedSymbol✝) "self" false✝)))))
Похожие утверждения