## Stream: new members

### Topic: Importing Packages

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

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 (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):

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

#### 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!

Last updated: May 14 2021 at 23:14 UTC