Where is data.real.basic?

Stream: new members

[Dan Piponi]

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]

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

[Dan Piponi]

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

[Dan Piponi]

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