# 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.

```text id="7a1pga"
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.

```lean id="tzut22"
theorem id_example (P : Prop) : P -> P := by
  intro h
  exact h
```

After `intro h`, the goal view shows:

```text id="yp4uro"
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.

```lean id="eurh2h"
#check Nat.succ
```

Hovering over `Nat.succ` shows:

```text id="oqp5tx"
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:

| Question                    | Where to look                 |
| --------------------------- | ----------------------------- |
| What assumptions do I have? | Local context                 |
| What must I prove?          | Target after `⊢`              |
| Why did this step fail?     | Error message near the cursor |

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.

```lean id="e7b080"
def addOne (n : Nat) : Nat :=
  _
```

The editor reports:

```text id="20k5nu"
n : Nat
⊢ Nat
```

For proofs:

```lean id="og2ut4"
theorem example (P : Prop) (h : P) : P := by
  _
```

The editor reports:

```text id="pkjofb"
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:

```lean id="65u64t"
#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:

```lean id="z36dyu"
Nat.
```

offers names in the `Nat` namespace.

Typing:

```lean id="dnl1zu"
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.

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

Expected output:

```text id="tx4c66"
[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:

```lean id="xx7phg"
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:

```text id="fz4hdd"
open: myproj/
```

Incorrect:

```text id="i51vud"
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:

```sh id="ag4xzb"
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:

```sh id="w30z5w"
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.

```sh id="krxq9c"
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.

```lean id="ozt2fn"
theorem and_swap (P Q : Prop) : P ∧ Q -> Q ∧ P := by
  _
```

Read the goal.

Introduce the hypothesis.

```lean id="7hzkmx"
  intro h
```

Read the new goal.

Build the conjunction.

```lean id="zudm6v"
  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.