Functor Array

Stream: lean4

[David Thrane Christiansen]

I'm curious as to why there's no instance like this by default:

instance : Functor Array where
  map := Array.map

As far as I can see, it satisfies the functor laws, preserves linearity as one would like, and is generally convenient.