1.24 Editor Integration

Lean is normally developed inside an editor with live feedback. The editor displays goals, local hypotheses, inferred types, and errors while the file is being written. This turns Lean from a batch compiler into an interactive proof environment.

Problem

You want to use the editor effectively: open the correct project, read the goal view, inspect terms, and avoid common tooling mistakes.

Solution

Use Visual Studio Code with the Lean extension, and open the project root directory.

myproj/
├── lakefile.lean
├── lean-toolchain
├── Myproj/
│   └── Basic.lean
└── Main.lean

Open myproj/, not only Myproj/Basic.lean. The editor needs the project root so it can find lakefile.lean, lean-toolchain, local modules, and dependencies.

Goal View

In tactic mode, the editor shows the current proof state.

theorem id_example (P : Prop) : P -> P := by
  intro h
  exact h

After intro h, the goal view shows:

P : Prop
h : P
⊢ P

The lines above ⊢ are the local context. The line after ⊢ is the target.

Hover Information

Hover over a name to inspect its type.

#check Nat.succ

Hovering over Nat.succ shows:

Nat.succ : Nat -> Nat

This is useful when using unfamiliar declarations.

Infoview Workflow

The infoview is the main feedback surface. Use it to answer three questions:

A good Lean workflow keeps the cursor near the line being developed and reads the infoview after each small step.

Holes in the Editor

A hole shows the expected type.

def addOne (n : Nat) : Nat :=
  _

The editor reports:

n : Nat
⊢ Nat

For proofs:

theorem example (P : Prop) (h : P) : P := by
  _

The editor reports:

P : Prop
h : P
⊢ P

The goal tells you what term the hole must contain.

Jump to Definition

Use the editor’s “Go to Definition” command on imported names.

Examples:

#check Nat.add
#check List.map
#check And.intro

This is one of the fastest ways to learn library APIs. It shows the actual declaration, surrounding namespace, and nearby lemmas.

Search and Completion

Autocomplete helps discover declarations.

Typing:

Nat.

offers names in the Nat namespace.

Typing:

List.

offers list operations and lemmas.

Completion is type-aware in many contexts, but it should not replace #check. Use completion to discover names and #check to confirm types.

Running Commands

Commands such as #check and #eval display results in the editor.

#check List.map
#eval List.map (fun n : Nat => n + 1) [1, 2, 3]

Expected output:

[2, 3, 4]

Use these commands as local probes while writing code.

Error Locations

Lean reports errors at the expression where elaboration failed. Sometimes the real cause is earlier.

Example:

def bad (n : Nat) : Nat :=
  n + true

The editor points to true, because addition expected a natural number there.

For longer expressions, replace subterms with holes or add type annotations until the error becomes local.

Opening the Correct Folder

Many editor problems come from opening the wrong folder.

Correct:

open: myproj/

Incorrect:

open: myproj/Myproj/

If the root is wrong, imports may fail even though the file itself exists.

Symptoms include:

• unresolved local imports
• missing dependencies
• wrong Lean version
• stale diagnostics

Restarting Lean

If diagnostics look stale, restart the Lean server from the editor command palette.

Before restarting, try:

lake build

The terminal build often gives a clearer project-level error.

Terminal and Editor Agreement

The editor and terminal should agree.

Check in the terminal:

lean --version
lake build

If the editor shows errors but lake build succeeds, restart the Lean server or check that the editor opened the project root.

If lake build fails, fix the build first. The editor depends on the same project configuration.

Using lake env

Some commands should be run inside the Lake environment.

lake env lean Myproj/Basic.lean

This ensures Lean sees the same paths and dependencies that Lake uses.

Common Pitfalls

If imports fail, open the project root and run lake build.

If the editor uses the wrong Lean version, inspect lean-toolchain.

If autocomplete misses local names, check whether the file has compiled up to that point.

If errors persist after a fix, restart the Lean server.

If a file is outside the project library, Lake may not know how to compile it.

Recipe: Editor-First Proof Development

Start with a theorem and a hole.

theorem and_swap (P Q : Prop) : P ∧ Q -> Q ∧ P := by
  _

Read the goal.

Introduce the hypothesis.

  intro h

Read the new goal.

Build the conjunction.

  constructor
  · exact h.right
  · exact h.left

Use the editor as a guide after each line.

Takeaway

The editor is part of the Lean workflow. It shows goals, types, errors, and library information continuously. Open the project root, keep the infoview visible, use holes and #check as probes, and confirm project health with lake build when diagnostics become unclear.