Lean4
/-- `Π₀ i, β i` denotes the type of dependent functions with finite support `DFinsupp β`. -/
@[term_parser 1000]
public meta def «termΠ₀_,_» : Lean.ParserDescr✝ :=
ParserDescr.node✝ `«termΠ₀_,_» 1022
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen (ParserDescr.symbol✝ "Π₀") Batteries.ExtendedBinder.extBinders)
(ParserDescr.symbol✝ ", "))
(ParserDescr.cat✝ `term 0))