Vector

Stream: general

[Jukka Suomela]

I see in many places references to the Vector type (fixed-size Array), which looks wonderful, but at least my Lean 4.14.0 doesn't seem to support it out-of-the-box unless I load some external libraries.

Am I just doing something wrong? Or is this something that is soon coming to Lean 4 core, just not yet? Or something that will require external libraries also in the future? And if external libraries are needed, should I be looking at mathlib, batteries, or something else (both mathlib and batteries seem to have some stuff related to Vector)?

[Edward van de Meent]

it seems to me that Vector (not List.Vector which was formerly known as Mathlib.Vector) is defined in the Init package, but was upstreamed from batteries about a month ago, and is currently part of v4.15.0-rc1.

[Edward van de Meent]

in short: you're not doing anything wrong, Vector isn't included out of the box for v4.14.0, but it seems it will be once v4.15.0 is released

[Jukka Suomela]

OK, wonderful, thanks, so I'll just wait for the next version update and start enjoying it after that! I had difficulties finding this kind of information anywhere online…

[Eric Wieser]

You can use it today if you add a dependency on batteries, or use v1.15.0rc1

[Jukka Suomela]

For me this would be just a convenience, so I can easily wait for the next version if I can that way avoid extra dependencies. :)

[Jukka Suomela]

(I also don't really understand this, but in batteries the lean-toolchain file currently says 4.15.0-rc1, so can I actually use the current version batteries without also switching to 4.15.0-rc1? I tried to use batteries with 4.14.0 and just got a pile of errors asking me to switch to 4.15.0-rc1.)

[Eric Wieser]

Batteries with 4.14.0 should be fine, if you have errors you can ask for help with them on #new members; it sounds like a configuration error somewhere on your side

[Kim Morrison]

To use Batteries with v4.14.0, you can't just require the main branch, you need to require the v4.14.0 tag.

[Jukka Suomela]

Yes, thanks, got help for it here: #new members > ✔ Batteries with Lean 4.14.0