Why is there both Vector and List.Vector?

Stream: lean4

[Geoffrey Irving]

I am uncertain about whether to use docs#Vector or docs#List.Vector, and why there are both of them.

[Geoffrey Irving]

Ah, I suppose implementationally the two would be very different (was working on a noncomputable project and forgot briefly).

[r.z. Almi.]

i think group affinities has something to do with it.
idk.

[Henrik Böving]

Geoffrey Irving said:

Ah, I suppose implementationally the two would be very different (was working on a noncomputable project and forgot briefly).

That is the difference yes

[Henrik Böving]

r. Almi. said:

i think group affinities has something to do with it.
idk.

I don't see how this would be related to the issue at hand at all?

[Eric Wieser]

Probably we should update the docstring for docs#List.Vector with "List.Vector is to Vector as List is to Array" or similar

[Kim Morrison]

#20693