You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
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.
The text was updated successfully, but these errors were encountered:
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.
The text was updated successfully, but these errors were encountered: