Lean4
/-- Dependent function type (a "pi type"). The notation `Π x ∈ s, β x` is
short for `Π x, x ∈ s → β x`. -/
-- A copy of forall notation from `Batteries.Util.ExtendedBinder` for pi notation
@[term_parser 1000]
public meta def «termΠ__,_» : Lean.ParserDescr✝ :=
ParserDescr.node✝ `PiNotation.«termΠ__,_» 1022
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen (ParserDescr.symbol✝ "Π ") (ParserDescr.parser✝ `Lean.Parser.Term.binderIdent))
(ParserDescr.cat✝ `binderPred 0))
(ParserDescr.symbol✝ ", "))
(ParserDescr.cat✝ `term 0))