Init not importing

Stream: general

[Frederick Pu]

It seems that Init isn't being imported properly when I don't have Mathlib or Batteries installed. Is that normal?

object file 'c:\Users\pufre\.elan\toolchains\leanprover--lean4---stable\lib\lean\Init\Data\Vector\Basic.olean' of module Init.Data.Vector.Basic does not exist

[Kim Morrison]

No, something is wrong. Can you post your lakefile and/or a link to a repo demonstrating this?

[Frederick Pu]

https://github.com/FrederickPu/TeryGrad/blob/main/TeryGrad/Minimal/Types.lean

[Kim Morrison]

Oh! There is no need to import anything in Init, it is all automatically imported for you.

[Frederick Pu]

im getting this tho: #check Vector

/-

unknown identifier 'Vector'
-/

[Kim Morrison]

Vector only arrived in Lean (core) in v4.15.0-rc1.

[Kim Morrison]

Put leanprover/lean4:v4.15.0-rc1 in your lean-toolchain.