English
Split a list according to the blocks of a composition: partition the list into sublists whose lengths are given by the blocks of the composition.
Русский
Разделить список по блокам композиции: разбить список на подсписки длины, заданные блоками композиции.
LaTeX
$$$\\mathrm{splitWrtComposition}: \\mathrm{List}\\,\\alpha \\to \\mathrm{Composition}(n) \\to \\mathrm{List}(\\mathrm{List}\\,\\alpha)$ with $\\mathrm{splitWrtComposition}(l,c) = \\mathrm{splitWrtCompositionAux}(l,c.blocks).$$$
Lean4
/-- Given a list of length `n` and a composition `[i₁, ..., iₖ]` of `n`, split `l` into a list of
`k` lists corresponding to the blocks of the composition, of respective lengths `i₁`, ..., `iₖ`.
This makes sense mostly when `n = l.length`, but this is not necessary for the definition. -/
def splitWrtComposition (l : List α) (c : Composition n) : List (List α) :=
splitWrtCompositionAux l c.blocks
