Importing Personal Files

Stream: general

[Brandon Sisler]

Heya all,
I was wondering if I had a file set up that looks like

Folder_Name
- stuff.lean
- cooler_stuff_that_needs_stuff.lean

then how can I import stuff.lean into cooler_stuff_that_needs_stuff.lean? Thanks! I imagine it must just be a quick thing, but I can't quite find the right syntax.

[Mauricio Collares]

If you haven't done so already, you have to create a project: Go into Folder_Name and type lake init Folder_Name. Then you can use import Folder_Name.stuff in the other file.