Multi-file lean4 project

Stream: new members

[Calvin Lee]

I haven't really seen any instruction on how to create a multi-file lean4 project. Is it necessary to have a leanpkg.toml?
I've tried to import from a second file multiple times and the language server can't seem to make sense of it.

[Bryan Gin-ge Chen]

Does this post help?

[Calvin Lee]

@Bryan Gin-ge Chen yes! thank you so much