English
For a list l of natural numbers, construct a list of lists l.ranges whose i-th inner list has length l_i, and whose concatenation equals the list of integers from 0 to sum(l)-1.
Русский
Для списка натуральных чисел l построим список списков l.ranges так, чтобы i-ий вложенный список имел длину l_i, а их объединение давало последовательность 0,1,2,..., сумма(l)-1.
LaTeX
$$$\mathrm{ranges}(l) \text{ is a List of Lists with } (l \text{).ranges} \text{ such that } (l.ranges).\text{map length} = l \text{ and } (l.ranges).\text{join} = \mathrm{range}(l.\text{sum})$$$
Lean4
/-- From `l : List ℕ`, construct `l.ranges : List (List ℕ)` such that `l.ranges.map List.length = l`
and `l.ranges.join = range l.sum`
* Example: `[1,2,3].ranges = [[0],[1,2],[3,4,5]]` -/
def ranges : List ℕ → List (List ℕ)
| [] => nil
| a :: l => range a :: (ranges l).map (map (a + ·))
