Mathlib/Data/Vector/Basic.lean

Stream: mathlib4

[Kim Morrison]

Would anyone be interested in doing a cleanup of List.Vector (previously named Mathlib.Vector)? It would be good to modernize this and give it an API that understands GetElem, as for List/Array/Vector.

[Shreyas Srinivas]

Can't it just be Vector from core with additional list like functions that use the list underlying the array inside the Vector?

[Shreyas Srinivas]

For example prepending elements would make more sense as a list operation than an array operation, so it would make sense to have it in List.Vector. Appending on the other hand should be already in core vector as an array operation

[Edward van de Meent]

Indeed, i suspect most mathlib people don't care about the precise difference between these definitions. especially since their behaviour at proof time should be pretty much equivalent.