Zulip Chat Archive

Stream: new members

Topic: intellisense


view this post on Zulip Michael Beeson (Sep 13 2020 at 18:33):

I split my lean file into three files and compiled the project. That solved the responsiveness problem, but now,
the proofs defined in the first two files no longer show up in intellisense when working on the third file, although of course
they ARE accessible if one can remember the spelling and order of arguments. How can I get them to show up in intellisense?

view this post on Zulip Alex Peattie (Sep 13 2020 at 22:38):

Hmm intellisense between files works OK for me (in VSCode) :thinking:. Do you have your project on a public repo by any chance?


Last updated: May 17 2021 at 22:15 UTC