Zulip Chat Archive

Stream: new members

Topic: Where is data.real.basic?

Dan Piponi (Nov 21 2021 at 00:10):

I'm trying to do the exercises at https://leanprover.github.io/theorem_proving_in_lean/quantifiers_and_equality.html#exercises I've installed elan on MacOS and run elan-init. I've worked through lots of exercises. But when I hit the one that involves data.real.basic lean fails with file 'data/real/basic' not found in the search path. How do I fix this?

Eric Wieser (Nov 21 2021 at 00:15):

Are you using leanproject? Do you have a leanpkg.toml containing a reference to mathlib (which it would create)?

Dan Piponi (Nov 21 2021 at 00:21):

I'm such a beginner I don't know what leanproject is

Dan Piponi (Nov 21 2021 at 00:24):

Cool! I typed leanproject new and now I get a sensible message. Thanks!

Last updated: Dec 20 2023 at 11:08 UTC