mkNotation — Mathlib

Lean4
/-- For `X : Truncated C n` and `m ≤ n`, `X ^⦋m⦌ₙ` is the `m`-th term of X. The
proof `p : m ≤ n` can also be provided using the syntax `X ^⦋m, p⦌ₙ`. -/
@[scoped term_parser 1000]
public meta def mkNotation : Lean.TrailingParserDescr✝ :=
  ParserDescr.trailingNode✝ `CategoryTheory.CosimplicialObject.Truncated.mkNotation 1024 0
    (ParserDescr.binary✝ `andthen
      (ParserDescr.binary✝ `andthen
        (ParserDescr.binary✝ `andthen
          (ParserDescr.binary✝ `andthen
            (ParserDescr.binary✝ `andthen (ParserDescr.symbol✝ " ^⦋") (ParserDescr.cat✝ `term 0))
            (ParserDescr.unary✝ `optional
              (ParserDescr.binary✝ `andthen (ParserDescr.symbol✝ ",") (ParserDescr.cat✝ `term 0))))
          (ParserDescr.symbol✝ "⦌"))
        (ParserDescr.const✝ `noWs))
      (ParserDescr.parser✝ `Mathlib.Tactic.subscriptTerm))
Похожие утверждения