[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.