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