1.22 Imports and Dependencies

Imports control what a Lean file can see. Dependencies control what a Lean project can use. Together, they define the environment in which definitions, theorems, tactics, notation, and instances are resolved.

Problem

You want to import declarations from other files, use external libraries, and keep project dependencies reproducible.

Solution

Use import at the top of a Lean file.

import Std

This makes declarations from Std available in the current file.

For a local module:

import Myproj.Basic

The module name must match the file path:

Myproj/Basic.lean

Local Imports

Suppose your project contains:

Myproj/
├── Basic.lean
└── Extra.lean

In Myproj/Basic.lean:

namespace Myproj

def double (n : Nat) : Nat :=
  n + n

end Myproj

In Myproj/Extra.lean:

import Myproj.Basic

#eval Myproj.double 10

Expected output:

20

The import gives Extra.lean access to declarations compiled from Basic.lean.

Imports Are Explicit

Lean does not search all files in a project automatically. If a declaration is in another module, import that module.

import Myproj.Basic

Without the import, Lean reports that the name is unknown.

This explicit model keeps dependencies visible and makes compilation predictable.

Import Order

Imports usually appear before all declarations.

import Std
import Myproj.Basic

namespace Myproj

The order matters when later imports depend on earlier ones, but ordinary files should avoid relying on subtle ordering effects. Prefer direct imports for the declarations you use.

Transitive Imports

If module A imports B, and B imports C, then A can often see declarations from C.

However, relying on transitive imports makes files fragile. If B later stops importing C, then A may break.

Prefer direct imports for important dependencies.

import Myproj.C
import Myproj.B

This makes the file’s requirements explicit.

Module Paths

The import path follows the directory structure.

The module name is case-sensitive. Keep directory names and module names aligned.

Dependencies in Lake

External dependencies are declared in lakefile.lean.

A minimal Lake file:

import Lake
open Lake DSL

package «myproj» where

lean_lib Myproj

To use an external dependency, add a require declaration.

require mathlib from git
  "https://github.com/leanprover-community/mathlib4"

Then run:

lake update
lake build

Lake records resolved dependencies in:

lake-manifest.json

Commit this file to make builds reproducible.

The Toolchain File

The file lean-toolchain pins the Lean version.

Example:

leanprover/lean4:stable

or:

leanprover/lean4:v4.12.0

When you run lean or lake, elan reads this file and chooses the matching toolchain.

For stable projects, prefer a specific version over stable.

Importing Mathlib

After adding mathlib as a dependency, import it in Lean files.

import Mathlib

This imports a large library and can increase build and elaboration time.

Prefer smaller imports when possible:

import Mathlib.Data.Nat.Basic
import Mathlib.Tactic

Small imports improve build performance and make dependencies clearer.

Dependency Hygiene

Good import hygiene follows a few rules:

Diagnosing Import Errors

If Lean reports:

unknown module prefix

check that:

• the file path matches the module name
• the file belongs to a declared lean_lib
• the project root is open in the editor
• lake build succeeds from the terminal

If Lean reports an unknown declaration after an import, the declaration may live in a different module. Use search tools in the editor or import the broader parent module temporarily.

Cyclic Imports

Imports must form an acyclic graph. This is invalid:

A imports B
B imports A

Fix cycles by extracting shared declarations into a third module.

Common
├── imported by A
└── imported by B

This keeps the dependency graph directed and compilable.

Recipe: Split a File into Modules

Start with one file:

Myproj/Basic.lean

Move reusable definitions into:

Myproj/Data.lean

Then import it:

import Myproj.Data

Keep theorem-heavy or example-heavy code in separate modules when possible.

Common Pitfalls

If imports work in the terminal but fail in the editor, open the project root folder.

If imports work on one machine but fail on another, compare lean-toolchain and lake-manifest.json.

If a file depends on a declaration only through a transitive import, add the direct import.

If importing all of Mathlib slows development, replace it with narrower imports.

If two modules need each other, move shared declarations to a third module.

Takeaway

Imports define the visible Lean environment for a file. Lake dependencies define the libraries available to the project. Keep imports explicit, module paths aligned with files, dependencies pinned, and the import graph acyclic. This gives Lean enough structure to compile predictably and gives readers enough information to understand where names come from.