typevec — Mathlib

Lean4
/-- simp set for the manipulation of typevec and arrow expressions -/
@[attr_parser 1000]
public meta def typevec : Lean.ParserDescr✝ :=
  ParserDescr.node✝ `Parser.Attr.typevec 1022
    (ParserDescr.binary✝ `andthen
      (ParserDescr.binary✝ `andthen
        (ParserDescr.binary✝ `andthen (ParserDescr.nonReservedSymbol✝ "typevec" false✝)
          (ParserDescr.unary✝ `optional
            (ParserDescr.binary✝ `orelse Lean.Parser.Tactic.simpPre Lean.Parser.Tactic.simpPost)))
        (ParserDescr.unary✝ `optional
          (ParserDescr.unary✝ `patternIgnore
            (ParserDescr.binary✝ `orelse (ParserDescr.nodeWithAntiquot✝ "← " `token.«← » (ParserDescr.symbol✝ "← "))
              (ParserDescr.nodeWithAntiquot✝ "<- " `token.«<- » (ParserDescr.symbol✝ "<- "))))))
      (ParserDescr.unary✝ `optional (ParserDescr.cat✝ `prio 0)))
Похожие утверждения