Importing Packages

Stream: new members

[Fredson Aguiar]

Hello!

I'm developing a package containing axioms, theorems and definitions, but I don't know how to build and import those new packages in my own local machine!

Are there any tutorial describing step by step?

[Kevin Buzzard]

Put everything in src and you should be able to import it fine. Take a look at the tutorial project

[Kevin Buzzard]

https://github.com/leanprover-community/tutorials

[Nam]

on importing packages, is there any reason for the imports to be restricted to the top of the files?

[Fredson Aguiar]

Sorry. I wasn't clear about what I needed. Files that are not inside a package themselves can still use dependencies, and this was my intention. But your answer guided me to my solution! Thanks so much!

[David⚛️]

Please how do I resolve this in Lean 3, I keep getting an error each time I try to import them
import data.real.basic
import data.real.nnreal

[Alex J. Best]

How did you set up the project you are working on (which commands did you follow?)

[David⚛️]

I got a lean file from GitHub I wanted opened in lean 3

[Eric Wieser]

Was the lean file from a github repo that contained other files?

[Eric Wieser]

If so, you should download the entire repo

[Alex J. Best]

Try following https://leanprover-community.github.io/leanproject.html, assuming you installed lean following https://leanprover-community.github.io/get_started.html