Stream: new members
Topic: Multi-file lean4 project
Calvin Lee (Jan 22 2021 at 16:47):
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 (Jan 22 2021 at 16:48):
Does this post help?
Calvin Lee (Jan 22 2021 at 17:02):
@Bryan Gin-ge Chen yes! thank you so much
Last updated: May 10 2021 at 00:31 UTC