Function that Replaces a List Element with another at an Idx

Stream: new members

[Colin ⚛️]

Is there a function that takes in an index and an element of the type represented in the List such that it replaces the element in the List at the index? It would look something like (n : ℕ) → (a : ?a) → List ?a → List ?a where n is the index and a is the object I want to put into the list.

For example, if 3 is the index given, 4:Nat is the object I want to replace the object in the list, and the list was [1,2,3,4], then the output would be [1,2,4,4].

[Arthur Paulino]

I think docs#List.modify does what you need

#eval [1, 2, 3, 4].modify (· + 10) 2 -- [1, 2, 13, 4]

[Evan Gao]

are you looking for List.set? If there are frequent modifications on the list then it's best to use an Array

[Aaron Liu]

@loogle Nat → List ?a → ?a → List ?a

[loogle]

:search: List.set, List.insertIdx, and 17 more