repeatList

Stream: lean4

[Igor Shimanogov]

In my commit to mathlib I need function

def repeatList.{u} {α : Type u} (n : Nat) (l : List α) : List α :=
  (List.replicate n l).flatten

It seems to be missing both in lean4 and mathlib, but there are several lemmas including this construction;

In Init:

1. List.flatten_replicate_nil
2. List.flatten_replicate_singleton
3. List.flatMap_replicate
4. List.flatten_replicate_replicate

And Mathlib:

1. List.getLast?_flatten_replicate
2. List.head?_flatten_replicate
3. List.ofFn_fin_repeat
4. FreeAddGroup.nsmul_mk
5. FreeGroup.pow_mk

Is it a good idea to make it a separate function and rewrite mentioned lemmas using new definition to get rid of repetitiveness?

[Kim Morrison]

Probably not? We don't want separate names for every combination of basic functions. This needlessly expands the API surface area.

[Eric Wieser]

Note that we do have docs#Fin.repeat