prodSyntax — Mathlib

Lean4
/-- `fbinop% f x y` elaborates `f x y` for `x : S α` and `y : S' β`, taking into account
any coercions that the "functors" `S` and `S'` possess. -/
@[term_parser 1000]
public meta def prodSyntax : Lean.ParserDescr✝ :=
  ParserDescr.node✝ `FBinopElab.prodSyntax 1024
    (ParserDescr.binary✝ `andthen
      (ParserDescr.binary✝ `andthen
        (ParserDescr.binary✝ `andthen
          (ParserDescr.binary✝ `andthen
            (ParserDescr.binary✝ `andthen (ParserDescr.symbol✝ "fbinop% ") (ParserDescr.const✝ `ident))
            (ParserDescr.const✝ `ppSpace))
          (ParserDescr.cat✝ `term 1024))
        (ParserDescr.const✝ `ppSpace))
      (ParserDescr.cat✝ `term 1024))
Похожие утверждения