mkNotation — Mathlib

Lean4
/-- For `m ≤ n`, `⦋m⦌ₙ` is the `m`-dimensional simplex in `Truncated n`. The
proof `p : m ≤ n` can also be provided using the syntax `⦋m, p⦌ₙ`. -/
@[scoped term_parser 1000]
public meta def mkNotation : Lean.ParserDescr✝ :=
  ParserDescr.node✝ `SimplexCategory.Truncated.mkNotation 1024
    (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))
Похожие утверждения