vscode-lean
vscode-lean copied to clipboard
leanprover
Make incomplete proofs more prominent
I've been working through mathematics in lean and I've found on the same page multiple incomplete proofs that I just didn't notice.
As it stands it puts a red squiggly under the by for a the tactics block.
It's pretty small and somewhat easy to miss.
How hard would it be to add something more prominent like the yellow squiggly when a proof uses sorry?
Maybe it's yellow when it uses sorry and red if it does not type check?
What are the thoughts on this.
I fully agree, and this is an issue for teaching especially. My workaround is to use the Error Lens VSCode extension, but this shouldn't be required.
We already have the progress indicator, projecting errors and other diagnostics onto that as well seems like a natural solution to me. Not sure if this should be changed in the server, as the client already has all relevant data for doing so.
