English
Given a list of binder terms, construct a pattern that is either the single binder or a nested tuple ⟨...⟩ of binders. This is a helper for forming binder patterns in expressions.
Русский
Учитывая наборBinder-термов, построить образец, который является либо единымBinder-термом, либо вложенной кортежной структурой ⟨...⟩; это вспомогательная функция для формирования образцов биндеров в выражениях.
LaTeX
$$$$ \\text{bigOpBindersPattern}(\\text{processed}) = \\begin{cases} \\text{ts}[0], & |\\text{ts}| = 1 \\\\ \\langle \\text{ts}, * \\rangle, & \\text{otherwise} \\end{cases} $$$$
Lean4
/-- Collects the binderIdents into a `⟨...⟩` expression. -/
def bigOpBindersPattern (processed : Array (Term × Term)) : MacroM Term := do
let ts := processed.map Prod.fst
if h : ts.size = 1 then
return ts[0]
else
`(⟨$ts,*⟩)
