Zulip Chat Archive

Stream: new members

Topic: Importing Packages

Fredson Aguiar (May 07 2020 at 00:06):


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 (May 07 2020 at 00:10):

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

Kevin Buzzard (May 07 2020 at 00:12):


Nam (May 07 2020 at 01:39):

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

Fredson Aguiar (May 07 2020 at 02:25):

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⚛️ (Mar 02 2023 at 17:03):

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 (Mar 02 2023 at 17:04):

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

David⚛️ (Mar 02 2023 at 18:41):

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

Eric Wieser (Mar 02 2023 at 18:44):

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

Eric Wieser (Mar 02 2023 at 18:44):

If so, you should download the entire repo

Alex J. Best (Mar 03 2023 at 01:55):

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

Last updated: Dec 20 2023 at 11:08 UTC