linarithArgsRest — Mathlib

Lean4
/-- Syntax for the arguments of `linarith`, after the optional `!`. -/
meta def linarithArgsRest : Lean.ParserDescr✝ :=
  ParserDescr.nodeWithAntiquot✝ "linarithArgsRest" `Mathlib.Tactic.linarithArgsRest
    (ParserDescr.binary✝ `andthen
      (ParserDescr.binary✝ `andthen Lean.Parser.Tactic.optConfig
        (ParserDescr.unary✝ `optional ((with_annotate_term"&" @ParserDescr.nonReservedSymbol✝) " only" false✝)))
      (ParserDescr.unary✝ `optional
        (ParserDescr.binary✝ `andthen
          (ParserDescr.binary✝ `andthen (ParserDescr.symbol✝ " [")
            ((with_annotate_term"sepBy(" @ParserDescr.sepBy✝) (ParserDescr.cat✝ `term 0) "," (ParserDescr.symbol✝ ", ")
              Bool.false✝))
          (ParserDescr.symbol✝ "]"))))
Похожие утверждения