English
Definition of an auxiliary function that, given a length n, a list l, a function f, and an accumulator r, returns a list built by applying f to all sublists of l of length n and concatenating with r.
Русский
Определение вспомогательной функции, которая по длине n, списку l, функции f и аккумулятору r строит список, состоящий из результатов применения f к всем подспискам l длины n, объединённых с r.
LaTeX
$$$\\operatorname{sublistsLenAux} : \\mathbb{N} \\to \\text{List}(\\alpha) \\to (\\text{List}(\\alpha) \\to \\beta) \\to \\text{List}(\\beta) \\to \\text{List}(\\beta)$$$$
Lean4
/-- Auxiliary function to construct the list of all sublists of a given length. Given an
integer `n`, a list `l`, a function `f` and an auxiliary list `L`, it returns the list made of
`f` applied to all sublists of `l` of length `n`, concatenated with `L`. -/
def sublistsLenAux : ℕ → List α → (List α → β) → List β → List β
| 0, _, f, r => f [] :: r
| _ + 1, [], _, r => r
| n + 1, a :: l, f, r => sublistsLenAux (n + 1) l f (sublistsLenAux n l (f ∘ List.cons a) r)
