tchajed/lean-zed
1
1
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity
Lean 4 syntax highlighting extension for Zed
1 commit 1 branch 0 tags 30 KiB
  • Tree-sitter Query 100%
Find a file
Exact
Tej Chajed 286afab510 Add Lean 4 syntax highlighting extension for Zed 
Tree-sitter based Lean 4 language support modeled on the VS Code Lean 4
extension's semantic-token vocabulary, powered by the tree-sitter-lean
grammar. Includes highlights, markdown injection in doc comments,
bracket matching, outline, indents, and folds.
2026-06-07 09:42:20 -07:00
languages/lean Add Lean 4 syntax highlighting extension for Zed 2026-06-07 09:42:20 -07:00
extension.toml Add Lean 4 syntax highlighting extension for Zed 2026-06-07 09:42:20 -07:00
README.md Add Lean 4 syntax highlighting extension for Zed 2026-06-07 09:42:20 -07:00

README.md

Lean for Zed

Syntax highlighting for the Lean 4 theorem prover in the Zed editor.

The highlighting is modeled on the VS Code Lean 4 extension: its capture vocabulary maps back to Lean's own SemanticTokenType set, so the colors line up with what the Lean LSP server emits at runtime. It is powered by the tree-sitter-lean grammar.

Features

  • Syntax highlighting (highlights.scm) — keywords, declarations, types, constructors, operators, literals, attributes, string interpolation, etc.
  • Markdown injection inside /-- … -/ doc comments (injections.scm).
  • Bracket matching, including Lean's ⟨ ⟩ and ⦃ ⦄ (brackets.scm).
  • Outline / symbol navigation for def, theorem, structure, inductive, namespace, … (outline.scm).
  • Auto-indent hints (indents.scm) and code folding (folds.scm).
  • .lean files, line comments (--) and block comments (/- … -/).

Scope

This is a static grammar for editor tooling, not a full reimplementation of Lean's extensible parser. User-defined notation / syntax / macro operators are only highlighted when they are part of the static operator table. When the Lean LSP server is attached, its semantic tokens take precedence; these queries provide the offline / cold-start floor.

Installing as a dev extension

  1. Clone this repository.
  2. In Zed open the command palette and run zed: install dev extension.
  3. Select this directory. Zed compiles the grammar and loads the language.
  4. Open any .lean file.

Development / testing

The Tree-sitter queries are validated against the grammar with the tree-sitter CLI:

# from a checkout of the tree-sitter-lean grammar repo
tree-sitter query /path/to/lean-zed/languages/lean/highlights.scm sample.lean

A successful run lists every capture (e.g. keyword.import, function, constructor, type.builtin, keyword.exception, …) with no query errors.