identOptScoped — Mathlib

Lean4
/-- `notation3` argument binding a name. -/
meta def identOptScoped : Lean.ParserDescr✝ :=
  ParserDescr.nodeWithAntiquot✝ "identOptScoped" `Mathlib.Notation3.identOptScoped
    (ParserDescr.binary✝ `andthen
      (ParserDescr.binary✝ `andthen (ParserDescr.const✝ `ident)
        (ParserDescr.unary✝ `optional
          (ParserDescr.binary✝ `andthen
            (ParserDescr.unary✝ `notFollowedBy
              (ParserDescr.unary✝¹ `group
                (ParserDescr.binary✝ `andthen
                  (ParserDescr.binary✝ `andthen (ParserDescr.symbol✝ ":") (ParserDescr.symbol✝ "("))
                  (ParserDescr.symbol✝ "scoped"))))
            (ParserDescr.parser✝ `Lean.Parser.precedence))))
      (ParserDescr.unary✝ `optional
        (ParserDescr.binary✝ `andthen
          (ParserDescr.binary✝ `andthen
            (ParserDescr.binary✝ `andthen
              (ParserDescr.binary✝ `andthen
                (ParserDescr.binary✝ `andthen
                  (ParserDescr.binary✝ `andthen (ParserDescr.symbol✝ ":") (ParserDescr.symbol✝ "("))
                  (ParserDescr.symbol✝ "scoped "))
                (ParserDescr.const✝ `ident))
              (ParserDescr.symbol✝ " => "))
            (ParserDescr.cat✝ `term 0))
          (ParserDescr.symbol✝ ")"))))
Похожие утверждения