Zulip Chat Archive

Stream: new members

Topic: Multi-file lean4 project


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

view this post on Zulip Bryan Gin-ge Chen (Jan 22 2021 at 16:48):

Does this post help?

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