List.fill

Stream: lean4

[Alex Sweeney]

A few times I needed a List of a fixed size initialized with a certain value so I wrote a simple List.fill.

def List.fill (a : α) (n : Nat) : List α :=
  fill a n []
where
  fill a : Nat → List α → List α
    | 0, as => as
    | n + 1, as => fill a n (a :: as)

#eval List.fill false 3
-- [false, false, false]

This is pretty common in other programming languages but I'm curious why it's not built into Lean. Is this not useful enough to belong in Lean's standard library?

[Alex Sweeney]

Or does it already exist and I clearly don't know how to find it?

[Damiano Testa]

Is docs#List.replicate what you were looking for?

[Patrick Massot]

Let me loogle this for you: https://loogle.lean-lang.org/?q=%3Fa+-%3E+Nat+-%3E+List+%3Fa

[Patrick Massot]

docs#List.replicate is indeed the second hit.

[Alex Sweeney]

Excellent, thanks!

[Scott Morrison]

It would not be insane to write a wrapper around exact? that "checked examples":

example : { f : Nat \to \a \to List \a // f 3 1 = [1, 1, 1] } := by spec?

This would synthesize terms for f by searching the library and then filter results by running rfl on the property.

[Scott Morrison]

In fact this should be pretty easy.