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.

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