VS Code extension manual

Stream: lean4

[Marc Huisinga]

In the most recent pre-release of the VS Code extension (0.0.154), you can now access a manual by navigating to 'Documentation'> 'Show Manual'. It covers most useful tools for working on Lean 4 code that are provided by the VS Code extension, VS Code and the Lean 4 language server.

If you don't have the pre-release, you can also already read it on GitHub at https://github.com/leanprover/vscode-lean4/blob/master/vscode-lean4/manual/manual.md.

[Patrick Massot]

Thanks Marc! This will be very useful to many people. I am sure that even long time users will learn things there.

[Kevin Buzzard]

Very nice! So do you think this is the place to put in capital letters "NOTE FOR BEGINNERS: TRY THESE SETTINGS* and explain how to turn off auto complete on enter?

[Steve Dunham]

For me, the hidden gem in Lean’s vscode settings is the ability to borrow its Unicode entry for other languages (like markdown).