VSCode "problems" with commands (#)

Stream: lean4

[Tomás Díaz]

Hi, I'm trying out the VSCode extension and checking the Theorem Proving book(?), and I get this indication that there are "problems" with # commands. I was wondering whether that's normal, why it happens, can it be disabled, etc? At a quick glance couldn't find any issues/references to this. It's not critical :lol: , but I find it a bit annoying (maybe it triggers some old memories, idk).
An example:
image.png
image.png

[Arthur Paulino]

"#" commands aren't supposed to be at the final state of your files. They are just helper commands, that you use while working but then get deleted after you're informed of what they say. For instance, if you define a function f and you want to test it with some inputs x y z, you might be able to use #eval f x y z just to see what it returns.

[Tomás Díaz]

perfect, thx :ok:

[Zhengying]

Hi there, I'm wondering how to use lean to prove a proposition such as 6 \in {6}. Which tactic should I use?

[Kevin Buzzard]

You should ask this in a separate thread, this thread is about VS Code problems in Lean 4. Are you talking about Lean 3? I would use library_search.