Lean4
/-- - `∑ x, f x` is notation for `Finset.sum Finset.univ f`. It is the sum of `f x`,
where `x` ranges over the finite domain of `f`.
- `∑ x ∈ s, f x` is notation for `Finset.sum s f`. It is the sum 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.sum (Finset.filter p s) f`.
- `∑ x ∈ s with h : p x, f x h` is notation for `Finset.sum s fun x ↦ if h : p x then f x h else 0`.
- `∑ (x ∈ s) (y ∈ t), f x y` is notation for `Finset.sum (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 bigsum : Lean.ParserDescr✝ :=
ParserDescr.node✝ `BigOperators.bigsum 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))
