[creata]

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

[derkha]

Lean 4 developer here. If the array is shared, we make a full copy. It's the same semantics as in Swift.

[creata]

Thanks. I assumed that option would be a major footgun (since accidental copies can be very expensive) but if it works for Swift, it can't be that bad.