leanprover / LeanInk

LeanInk is a command line helper tool for Alectryon which aims to ease the integration of Lean 4.
Apache License 2.0
60 stars 16 forks source link

Red squiggles #34

Open lovettchris opened 2 years ago

lovettchris commented 2 years ago

Current behaviour

for code that contains error we get this, and the hover tip correctly shows the error, but there is no visual clue of any error in this code:

image

Suggested behaviour

VS Code shows this which is nicer:

image

Reasoning

Additional notes