How to apply a function to first i elements of a list

Stream: new members

[Shaojun Zhang]

just like the title, if i have a function

$$f : A \rightarrow B$$

and a List A

$$L = [a_1, a_2, \cdots, a_n]$$

how can iget

$$L' = [f (a_1), f (a_2), \cdots, f (a_i), a_{i+1}, \cdots, a_n]$$

I think there is such a function in the Mathlib, but I can't find it

[Kevin Buzzard]

Can you write the question in lean? The naive approach doesn't work because L doesn't have type List A or List B. So right now the question is kind of undefined

[Eric Wieser]

docs#List.splitAt is probably the main thing you want

[Shaojun Zhang]

Kevin Buzzard said:

Can you write the question in lean? The naive approach doesn't work because L" doesn't have type List A or List B. So right now the question is kind of undefined

emm, I wrote it wrong above. It should be like following

def List.mapi {A : Type} (L : List A) (f : A -> A) (i : Fin L.length) :=
  (List.map f (L.take i)) ++ L.drop i

[Kevin Buzzard]

If you write it in Lean then you can't write it wrong :-)