Lean4
@[inherit_doc torusIntegral, term_parser 1000]
public meta def «term∯_InT(_,_),_» : Lean.ParserDescr✝ :=
ParserDescr.node✝ `«term∯_InT(_,_),_» 1022
(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✝ "∯") Batteries.ExtendedBinder.extBinders)
(ParserDescr.symbol✝ " in "))
(ParserDescr.symbol✝ "T("))
(ParserDescr.cat✝ `term 0))
(ParserDescr.symbol✝ ", "))
(ParserDescr.cat✝ `term 0))
(ParserDescr.symbol✝ ")"))
(ParserDescr.symbol✝ ", "))
(ParserDescr.cat✝ `term 0))