repeat list

Stream: Is there code for X?

[Aaron Liu]

Concatenate a list to itself n times, like this

def repeatList.{u} {α : Type u} (n : Nat) (l : List α) : List α :=
  match n with
  | 0 => []
  | n + 1 => l ++ repeatList n l

or like this

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

[Michael Rothgang]

You have seen docs#List.replicate, right? (That's not what you're asking for, but perhaps loogling for that is more helpful.)

[Aaron Liu]

I have seen it, I even used it in one of the example implementations!

[Aaron Liu]

Unfortunately loogle isn't giving any results :(

[Michael Rothgang]

I also looked at the hits: all of this seems about repeating a single list.

[Eric Wieser]

Here's another:

def repeatList.{u} {α : Type u} (n : Nat) (l : List α) : List α :=
  (FreeMonoid.ofList l ^ n).toList

[Aaron Liu]

That depends on mathlib!

[Eric Wieser]

You seem to use mathlib quite a lot so I figured that would be ok!

[Eric Wieser]

(List.replicate n l).flatten seems fairly idiomatic to me

[Aaron Liu]

Eric Wieser said:

You seem to use mathlib quite a lot so I figured that would be ok!

Mathlib is quite useful, but I don't want to import the free monoid in some list code

[Bernhard Reinke]

(List.replicate n l).flatten is indeed idiomatic, some helper lemmas are stated in this form, see for example this loogle query

[Igor Shimanogov]

Needed the same repeatList in https://github.com/leanprover-community/mathlib4/pull/24441
Is it good idea to make a separate function in mathlib and rewrite all lemmas from that loogle query using this definition?

[Michael Rothgang]

I'd say: The lemmas in Init are in Lean core and should definitely stay. The two hits in mathlib, maybe.

[Eric Wieser]

I think perhaps the question should be whether this function should exist in Lean core, but that's a question for #lean4