Zulip Chat Archive

Stream: new members

Topic: import data.nat.basic gives an error


view this post on Zulip slwkB (Jan 30 2021 at 19:41):

Hey, it will be my first question :) I'm going through exercises from https://leanprover.github.io/theorem_proving_in_lean/theorem_proving_in_lean.pdf . Exercise 4 from section 4.6 requires aforementioned import. But what I get is "invalid import: data.nat.basic could not resolve import: data.nat.basic". My version is:
Lean (version 3.24.0, commit 13007ebb4de6, Release)
It was installed with instruction from https://leanprover-community.github.io/install/macos.html (via curl). The question is what am I doing wrong, or what configurational step did I miss?

view this post on Zulip Kevin Buzzard (Jan 30 2021 at 19:49):

Is there not a URL in the error message which lists the standard mistakes beginners have made when imports don't work?

view this post on Zulip slwkB (Jan 30 2021 at 19:57):

There is indeed, but it was as another error not expanded in vs code infoview when I selected the line with import :see_no_evil:

view this post on Zulip Bryan Gin-ge Chen (Jan 30 2021 at 20:46):

You'll have to create a project that depends on mathlib in order to import data.nat.basic (and this should probably be mentioned explicitly in TPiL, cc: @Jeremy Avigad ). See the steps on the "Lean projects" page.

view this post on Zulip Jeremy Avigad (Jan 30 2021 at 22:43):

Good point. The "about Lean" section is really outdated. https://leanprover.github.io/theorem_proving_in_lean/introduction.html#about-lean
I think it would be helpful there to:

  • mention mathlib
  • explain that TPIL focuses on core aspects of Lean rather than mathlib
  • point out that, nonetheless, parts of it rely on importing files from mathlib
  • point to the Lean community web pages for information on installing Lean and setting up a mathlib project
  • point to the Lean community web pages for documentation of mathlib.

Would that address this particular issue? Is there anything else that should go in that section?

view this post on Zulip Bryan Gin-ge Chen (Jan 30 2021 at 22:55):

That looks good to me, thanks!


Last updated: May 16 2021 at 21:11 UTC