VS Code + Latex input usability

Stream: lean4

[Tom]

Just a note on VSCode - there is a small extension that I've used for a while: latex-input. It allows one to insert one-off latex characters while coding.

I've mostly used this for documentation with other languages but it's even nicer with Lean because once you type \, it will help with autocompletion. I find it complementary to the the "Lean 4: Show All Abbreviations" command/help.

Perhaps others will find it useful, too.

[Siddhartha Gadgil]

Thanks for this. When making slides, blogs etc for lean I keep copying code from lean but I can now just type the LaTeX.