Zulip Chat Archive

Stream: new members

Topic: Importing Packages


view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (May 07 2020 at 00:12):

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

view this post on Zulip 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?

view this post on Zulip 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