Lean has an array type, which the docs say is implemented much like a C++ vector or Rust Vec. But data types in functional programming languages all expose an immutable interface, so what happens when someone changes the list in two different ways? Is a new copy of the array made, is some variant of a persistent array used, or does the program just fail to compile?

https://leanprover.github.io/lean4/doc/array.html