reading the library

Stream: general

[Michael Beeson]

I opened core.lean in VSC and was surprised to see that it generates errors. Is that correct behavior? How can I open
the library source files and not see errors?

[Yury G. Kudryashov]

Did you fetch oleans? The easiest way is to use leanproject up from mathlib-tools

[Kevin Buzzard]

I think he's talking about core, not mathlib

[Yury G. Kudryashov]

Ah, sorry.

[Yury G. Kudryashov]

Wild guess: VSC tries wrong version of Lean. Don't know how to verify this.

[Patrick Massot]

In your project that works, write #check nat and right-click on nat, choose Go to definition

[Patrick Massot]

This way you'll end up in the right place