New to Lean, Blue Squiggle in VS Code

Stream: new members

[Dave Jones]

Hello, very new Lean user here

I've been able to get everything installed and work through some basic proofs successfully
I'm noticing in VS Code that although #eval and #check statements are displaying the expected output in infoview, these lines display with a blue squiggle underneath and show up in the "Problems" pane of VS Code (without any additional information given).

I suspect this indicates that something may be set up incorrectly, but the Lean project appears to be ok. I've tried restarting VS Code and issuing a Lean: Restart command, but it hasn't helped.

Any pointers would be appreciated. Thanks in advance.

[Vincent Beffara]

Blue squiggle is fine! (It shows up as "info", the fact that the pane is called "problems" is a bit misleading.)

[Dave Jones]

Thank you for the quick reply - ah so this is the expected behavior?
That would be reassuring.

[Vincent Beffara]

Yes, it is expected behavior, your system is working