simpsOptAttrOption — Mathlib

Lean4
/-- An `(attr := ...)` option for `simps`. -/
meta def simpsOptAttrOption : Lean.ParserDescr✝ :=
  ParserDescr.nodeWithAntiquot✝ "simpsOptAttrOption" `Lean.Parser.Attr.simpsOptAttrOption
    (ParserDescr.unary✝ `optional
      (ParserDescr.unary✝ `atomic
        (ParserDescr.binary✝ `andthen
          (ParserDescr.binary✝ `andthen
            (ParserDescr.binary✝ `andthen
              (ParserDescr.binary✝ `andthen (ParserDescr.symbol✝ " (")
                ((with_annotate_term"&" @ParserDescr.nonReservedSymbol✝) "attr" false✝))
              (ParserDescr.symbol✝ " := "))
            ((with_annotate_term"sepBy(" @ParserDescr.sepBy✝) (ParserDescr.parser✝ `Lean.Parser.Term.attrInstance) ","
              (ParserDescr.symbol✝ ", ") Bool.false✝))
          (ParserDescr.symbol✝ ")"))))
Похожие утверждения