def List.toArrayMap {α : Type u} {β : Type v} (l : List α) (f : α → β) : Array β

This function is provided as a more efficient runtime alternative to (l.map f).toArray. (It avoids the intermediate memory allocation of creating an intermediate list first.) For verification purposes, we immediately simplify it to that form.

Equations

• l.toArrayMap f = List.foldl (fun (acc : Array β) (x : α) => acc.push (f x)) #[] l

theorem List.toArrayMap_toList {α : Type u} {β : Type v} (l : List α) (f : α → β) : (l.toArrayMap f).toList = map f l

@[simp]

theorem List.toArrayMap_eq_toArray_map {α : Type u} {β : Type v} (l : List α) (f : α → β) : l.toArrayMap f = (map f l).toArray