English
Given an array of binder pairs, assemble the overall product by iterated SProd operations; the empty case yields the universal binder, and the singleton case returns the single binder block.
Русский
Дано множество пар Binder и объединяем итоговый продукт последовательной операцией SProd; пустой случай даёт всеобщий Binder, одиночный случай — единственный блок.
LaTeX
$$$$ \\text{BigOpBindersProd}(\\text{processed}) = \\begin{cases} \\mathsf{Finset.univ}, & |\\text{processed}|=0 \\\\ \\text{second component of processed}[0], & |\\text{processed}|=1 \\\\ \\text{fold over processed with } SProd, & \\text{otherwise} \\end{cases} $$$$
Lean4
/-- Collects the terms into a product of sets. -/
def bigOpBindersProd (processed : Array (Term × Term)) : MacroM Term := do
if h₀ : processed.size = 0 then
`((Finset.univ : Finset Unit))
else if h₁ : processed.size = 1 then
return processed[0].2
else
processed.foldrM (fun s p => `(SProd.sprod $(s.2) $p)) processed.back.2 (start := processed.size - 1)
