foldAction — Mathlib

Lean4
/-- `notation3` argument simulating a Lean 3 fold notation. -/
meta def foldAction : Lean.ParserDescr✝ :=
  ParserDescr.nodeWithAntiquot✝ "foldAction" `Mathlib.Notation3.foldAction
    (ParserDescr.binary✝ `andthen
      (ParserDescr.binary✝ `andthen
        (ParserDescr.binary✝ `andthen
          (ParserDescr.binary✝ `andthen
            (ParserDescr.binary✝ `andthen
              (ParserDescr.binary✝ `andthen
                (ParserDescr.binary✝ `andthen
                  (ParserDescr.binary✝ `andthen
                    (ParserDescr.binary✝ `andthen
                      (ParserDescr.binary✝ `andthen
                        (ParserDescr.binary✝ `andthen
                          (ParserDescr.binary✝ `andthen
                            (ParserDescr.binary✝ `andthen
                              (ParserDescr.binary✝ `andthen
                                (ParserDescr.binary✝ `andthen
                                  (ParserDescr.binary✝ `andthen (ParserDescr.symbol✝ "(") (ParserDescr.const✝ `ident))
                                  (ParserDescr.const✝ `ppSpace))
                                (ParserDescr.parser✝ `Lean.Parser.strLit))
                              (ParserDescr.symbol✝ "*"))
                            (ParserDescr.unary✝ `optional (ParserDescr.parser✝ `Lean.Parser.precedence)))
                          (ParserDescr.symbol✝ " => "))
                        Mathlib.Notation3.foldKind)
                      (ParserDescr.symbol✝ " ("))
                    (ParserDescr.const✝ `ident))
                  (ParserDescr.const✝ `ppSpace))
                (ParserDescr.const✝ `ident))
              (ParserDescr.symbol✝ " => "))
            (ParserDescr.cat✝ `term 0))
          (ParserDescr.symbol✝ ") "))
        (ParserDescr.cat✝ `term 0))
      (ParserDescr.symbol✝ ")"))
Похожие утверждения