Covers syntax for Lean 3, an interactive theorem prover at https://leanprover-community.github.io/ whose users mostly use VSCode.