Zulip Chat Archive

Stream: general

Topic: reading the library


Michael Beeson (Apr 17 2020 at 16:53):

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 (Apr 17 2020 at 16:56):

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

Kevin Buzzard (Apr 17 2020 at 16:56):

I think he's talking about core, not mathlib

Yury G. Kudryashov (Apr 17 2020 at 16:56):

Ah, sorry.

Yury G. Kudryashov (Apr 17 2020 at 16:57):

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

Patrick Massot (Apr 17 2020 at 16:58):

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

Patrick Massot (Apr 17 2020 at 16:58):

This way you'll end up in the right place


Last updated: Dec 20 2023 at 11:08 UTC