Highlight proven (processed) regions of Lean 4 files in green, like VSRcoq.
Works on top of the official Lean 4 extension.
Quick start
| Step | Action |
|---|---|
| 1 | Install Lean 4 + this extension |
| 2 | Open a .lean file — processed code turns green automatically |
| 3 | Alt+↓ / Alt+↑ — step through processed blocks manually |
| 4 | Alt+R — reset to follow the server again |
Features
- Auto‑highlight — the proven prefix (from file start to the latest processed position) gets a translucent green background as Lean verifies your code.
- Manual stepping —
Alt+↓/Alt+↑move the "frontier" without moving code, letting you inspect the proof state at each step boundary. - Two step modes (toggle via Command Palette):
- Atomic — step through every incremental fragment the server reported (more granular).
- Merged — step through the server's merged processed ranges.
- Reset (
Alt+R) — back to auto‑follow. - Diagnostic output — open View → Output → "Lean Processed Highlighter" to see real‑time progress.
Commands & shortcuts
| Shortcut | Command | Action |
|---|---|---|
Alt+↓ |
Lean4: Step Highlight Forward |
Next processed block |
Alt+↑ |
Lean4: Step Highlight Backward |
Previous / current block start |
Alt+R |
Lean4: Reset Highlight To Server State |
Reset to auto‑follow |
All commands are also available via Ctrl+Shift+P → Lean4: ....
| ID | Title |
|---|---|
lean4Processed.toggle |
Toggle Processed Highlight |
lean4Processed.highlightNow |
Highlight Processed Region Now |
lean4Processed.stepForward / stepBackward |
Step Highlight Forward / Backward |
lean4Processed.reset / followServer |
Reset / Follow Server Progress |
lean4Processed.toggleStepMode |
Toggle Step Mode (Atomic / Merged) |
Requirements
- VS Code ≥ 1.75 (same requirement as the Lean 4 extension)
- Lean 4 extension (
leanprover.lean4) installed and active
License
MIT