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