feat: upstream definition of Vector from Batteries

leanprover / lean4

Lean 4 programming language and theorem prover

https://lean-lang.org

Apache License 2.0

4.75k stars 427 forks source link

feat: upstream definition of Vector from Batteries #6197

Closed kim-em closed 4 days ago

kim-em commented 5 days ago

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

leanprover-community-bot commented 5 days ago

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 commented 4 days ago

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 commented 4 days ago

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 commented 4 days ago

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.