Stream: new members
Alexandre Rademaker (Sep 17 2020 at 01:25):
I follow the steps from https://leanprover-community.github.io/install/project.html, I opened the VS Code and I am getting this error, any idea?
Alexandre Rademaker (Sep 17 2020 at 01:30):
OK, this is strange... It is working with Emacs...
Bryan Gin-ge Chen (Sep 17 2020 at 01:34):
You opened the entire
my_project/ directory in VS Code, right? If you try to open just a standalone file the extension won't be able to find mathlib.
Alexandre Rademaker (Sep 17 2020 at 03:03):
Thank you, now it is clear that I need to open the complete directory not only the file.
Last updated: May 14 2021 at 04:22 UTC