Zulip Chat Archive
Stream: lean4
Topic: VSCode error message
Kenny Lau (Jan 05 2021 at 15:47):
How do I view the error messages on VSCode?
Edward Ayers (Jan 05 2021 at 15:49):
I can see the errors in the 'problems' pane. I am using the vscode extension mhuisi.lean4
Edward Ayers (Jan 05 2021 at 15:50):
Following your intructions at 'How to install Lean 4'
Kenny Lau (Jan 05 2021 at 15:51):
oh, that works
Kenny Lau (Jan 05 2021 at 15:51):
I was just used to the "All Messages" window that exists for Lean 3
Edward Ayers (Jan 05 2021 at 15:51):
It's back to basics for a while I guess
Edward Ayers (Jan 05 2021 at 15:52):
You can also whack F8 and it will show the error message inline
Last updated: Dec 20 2023 at 11:08 UTC