Zulip Chat Archive

Stream: new members

Topic: intellisense

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?

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: Dec 20 2023 at 11:08 UTC