| ← Installing the toolchain | Index | Next: A note on Mathlib → |
Install the Lean 4 extension for VS Code. It provides:
- Inline goal state (the “Lean infoview”) while writing proofs.
- Jump-to-definition (the editor command that navigates to where a name was originally introduced) for anything in core Lean or Mathlib.
- Red squiggles marking errors inline, plus autocomplete suggestions during typing.
| ← Installing the toolchain | Index | Next: A note on Mathlib → |