Lean4
/-- - `∏ x, f x` is notation for `Finset.prod Finset.univ f`. It is the product of `f x`,
where `x` ranges over the finite domain of `f`.
- `∏ x ∈ s, f x` is notation for `Finset.prod s f`. It is the product of `f x`,
where `x` ranges over the finite set `s` (either a `Finset` or a `Set` with a `Fintype` instance).
- `∏ x ∈ s with p x, f x` is notation for `Finset.prod (Finset.filter p s) f`.
- `∏ x ∈ s with h : p x, f x h` is notation for
`Finset.prod s fun x ↦ if h : p x then f x h else 1`.
- `∏ (x ∈ s) (y ∈ t), f x y` is notation for `Finset.prod (s ×ˢ t) (fun ⟨x, y⟩ ↦ f x y)`.
These support destructuring, for example `∏ ⟨x, y⟩ ∈ s ×ˢ t, f x y`.
Notation: `"∏" bigOpBinders* ("with" (ident ":")? term)? "," term` -/
@[term_parser 1000]
public meta def bigprod : Lean.ParserDescr✝ :=
ParserDescr.node✝ `BigOperators.bigprod 1022
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen (ParserDescr.symbol✝ "∏ ") BigOperators.bigOpBinders)
(ParserDescr.unary✝ `optional
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen (ParserDescr.symbol✝ " with ")
(ParserDescr.unary✝ `optional
(ParserDescr.unary✝ `atomic
(ParserDescr.binary✝ `andthen Lean.binderIdent (ParserDescr.symbol✝ " : ")))))
(ParserDescr.cat✝ `term 0))))
(ParserDescr.symbol✝ ", "))
(ParserDescr.cat✝ `term 67))
