feat: upstream definition of Vector from Batteries

[kim-em]

This PR upstreams the definition of Vector from Batteries, along with the basic functions.

[leanprover-community-bot]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 4e885be96d82c522af4acb9ce9afe77e5aea7feb --onto ba3f2b3ecf8967410f3498e2835b883601f03967. (2024-11-24 10:14:20)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 4e885be96d82c522af4acb9ce9afe77e5aea7feb --onto 884a9ea2ff70bb4d0c6da4a1c23ffc26c3a974ee. (2024-11-24 22:58:11)

[tydeu]

Out of curiosity, is the plan to eventually have a native implementation of Vector (since it can be more efficiently represented than an Array)?

[nomeata]

Out of curiosity, is the plan to eventually have a native implementation of Vector (since it can be more efficiently represented than an Array)?

Can it? You still need the length information at runtime for things like compactification

[digama0]

Indeed. You need the capacity at runtime for GC to work correctly, although you could drop the length field at the cost of making push a major performance footgun.