Lean4
/-- `Πʳ i, [R i, A i]_[𝓕]` is `RestrictedProduct R A 𝓕`. -/
@[scoped term_parser 1000]
public meta def «termΠʳ_,[_,_]_[_]» : Lean.ParserDescr✝ :=
ParserDescr.node✝ `RestrictedProduct.«termΠʳ_,[_,_]_[_]» 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.binary✝ `andthen (ParserDescr.symbol✝ "Πʳ") Batteries.ExtendedBinder.extBinders)
(ParserDescr.symbol✝ ", "))
(ParserDescr.symbol✝ "["))
(ParserDescr.cat✝ `term 0))
(ParserDescr.symbol✝ ", "))
(ParserDescr.cat✝ `term 0))
(ParserDescr.symbol✝ "]_["))
(ParserDescr.cat✝ `term 0))
(ParserDescr.symbol✝ "]"))