intellisense

Stream: new members

[Michael Beeson]

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]

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