In Lean, when I define a structure like this

structure Point where
  x : Float
  y : Float

and then I work with an Array Point I understand that at runtime each Point is allocated on the heap and the array stores a contiguous region of memory that contains pointers to the Points.

Is there a way to tell the Lean compiler to allocate the whole array (including the Points) in a single memory region similar to how it would be done in C++ or Rust? I belive in Haskell this can achieved using Data.Vector.Unboxed.

Does the Lean compiler already do this transformation as part of its optimizations? If yes, under which conditions?