Zulip Chat Archive

Stream: new members

Topic: import data.nat.basic gives an error


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?

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?

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:

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.

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?

Bryan Gin-ge Chen (Jan 30 2021 at 22:55):

That looks good to me, thanks!


Last updated: Dec 20 2023 at 11:08 UTC