uncaught exception: unknown package 'Examples' error #3
Description
I am getting this error while trying to run the first notebook (part 1, notebook 1). I am not sure if this is a VS code bug or if there is something I am missing. Lean seems to work as usual on Example0.lean file.
The suggestion above didn't work.
Tried lean update on the directory, didn't work
Tried to clear VS code cache with "clear editor history"
Tried to update Elan didn't work
Tried restarting the lean language server, didn't work either.
Any suggestion is much appreciated.
Edit: I asked someone else to try it as well, they had the same error.