Array vs List

Stream: lean4

[Tanner Swett]

As far as the observable and provable behavior go, Array and List are pretty much identical, right?

Behind the scenes, it looks like Array is a resizable mutable array that gets copied as necessary, whereas List is a linked list, right?

[James Gallicchio]

Array is modeled as a List (see the Array structure), so for proof purposes they are essentially the same.

[Tanner Swett]

Aha, very nice.