setArgsRest — Mathlib

Lean4
meta def setArgsRest : Lean.ParserDescr✝ :=
  ParserDescr.nodeWithAntiquot✝ "setArgsRest" `Mathlib.Tactic.setArgsRest
    (ParserDescr.binary✝ `andthen
      (ParserDescr.binary✝ `andthen
        (ParserDescr.binary✝ `andthen
          (ParserDescr.binary✝ `andthen
            (ParserDescr.binary✝ `andthen (ParserDescr.const✝ `ppSpace) (ParserDescr.const✝ `ident))
            (ParserDescr.unary✝ `optional
              (ParserDescr.binary✝ `andthen (ParserDescr.symbol✝ " : ") (ParserDescr.cat✝ `term 0))))
          (ParserDescr.symbol✝ " := "))
        (ParserDescr.cat✝ `term 0))
      (ParserDescr.unary✝ `optional
        (ParserDescr.binary✝ `andthen
          (ParserDescr.binary✝ `andthen (ParserDescr.symbol✝ " with ")
            (ParserDescr.unary✝ `optional (ParserDescr.symbol✝ "← ")))
          (ParserDescr.const✝ `ident))))
Похожие утверждения