## 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):

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: May 16 2021 at 21:11 UTC