bigOpBinder — Mathlib

Lean4
/-- A `bigOpBinder` is like an `extBinder` and has the form `x`, `x : ty`, or `x pred`
where `pred` is a `binderPred` like `< 2`.
Unlike `extBinder`, `x` is a term. -/
meta def bigOpBinder : Lean.ParserDescr✝ :=
  ParserDescr.nodeWithAntiquot✝ "bigOpBinder" `BigOperators.bigOpBinder
    (ParserDescr.binary✝ `andthen (ParserDescr.cat✝ `term 1024)
      (ParserDescr.unary✝ `optional
        (ParserDescr.binary✝ `orelse
          (ParserDescr.unary✝¹ `group
            (ParserDescr.binary✝ `andthen (ParserDescr.symbol✝ " : ") (ParserDescr.cat✝ `term 0)))
          (ParserDescr.cat✝ `binderPred 0))))
Похожие утверждения