termΠ__,_ — Mathlib

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))
Похожие утверждения