Lean4
@[inherit_doc ContMDiffSection, scoped term_parser 1000]
public meta def «termCₛ^_⟮_;_,_⟯» : Lean.ParserDescr✝ :=
ParserDescr.node✝ `Manifold.«termCₛ^_⟮_;_,_⟯» 1024
(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✝ "Cₛ^") (ParserDescr.cat✝ `term 0))
(ParserDescr.symbol✝ "⟮"))
(ParserDescr.cat✝ `term 0))
(ParserDescr.symbol✝ "; "))
(ParserDescr.cat✝ `term 0))
(ParserDescr.symbol✝ ", "))
(ParserDescr.cat✝ `term 0))
(ParserDescr.symbol✝ "⟯"))