Direction of List.map_toArray vs Array.toList_map

Stream: lean4

[Eric Wieser]

I'm a little surprised that docs#List.map_toArray and docs#Array.toList_map are both simp, yet push their functions in opposite directions. I think in mathlib we almost always push these kinds of functions from the outside in (matching toList_map), and make the user apply toArray_inj or similar iff they want to go the opposite way.