Split list to chunks of specified size

Stream: Is there code for X?

[Daniel Weber]

Suppose I have a list l : List α, and a sz : List Nat such that sz.sum = l.length. How can I split l to chunks according to the sizes specified by sz? For example, for l = [a, b, c, d], sz = [1,0,0,2,0,1] I want to get [[a], [], [], [b, c], [], [d]]

[Bryan Gin-ge Chen]

Something like this?

def foo : List α → List Nat → List (List α)
| _, [] => []
| x, n::ns =>
  let (x0, x1) := x.splitAt n
  x0 :: foo x1 ns

#eval foo [0,1,2,3] [1,0,0,2,0,1] -- [[0], [], [], [1, 2], [], [3]]

[Daniel Weber]

Yes, thanks

[Kim Morrison]

Someone was recently writing some API for run length encoding. Perhaps it would be useful to see where that got to.

[Daniel Weber]

What would be a good file in Mathlib for this definition?

[Kim Morrison]

If it's called List.splitLengths, then Mathlib.Data.List.SplitLengths?

[Daniel Weber]

#17191

[Kim Morrison]

Daniel Weber said:

#17191

:writing: