1.3 Files, Namespaces, and Modules

Lean organizes code as a hierarchy of modules. A module corresponds to a file, and a namespace provides a logical grouping of declarations inside that file. Correct use of files, namespaces, and imports determines whether a project remains manageable as it grows.

Problem

You want a consistent way to organize code so that names are predictable, imports resolve correctly, and large developments remain navigable.

Solution

Use a one-to-one mapping between file paths and module names, and use namespaces to structure declarations within modules.

A file:

Myproj/Algebra/Group.lean

defines the module:

import Myproj.Algebra.Group

Inside the file, define a namespace that reflects the logical structure:

namespace Myproj.Algebra

structure Group where
  carrier : Type
  mul : carrier -> carrier -> carrier

end Myproj.Algebra

Modules

A module is the unit of compilation. Each .lean file is compiled independently, subject to its imports.

Properties:

• modules form a directed acyclic graph via imports
• a module only sees declarations from imported modules
• recompilation follows the import graph

Imports must appear at the top of the file:

import Myproj.Basic
import Myproj.Algebra.Group

There is no implicit import. If a name is not found, the module that defines it has not been imported.

Namespaces

A namespace groups related declarations and prevents name collisions.

namespace Myproj

def x : Nat := 1

end Myproj

The fully qualified name is:

Myproj.x

Namespaces can be nested:

namespace Myproj.Algebra

def id {G : Type} (x : G) := x

end Myproj.Algebra

This produces:

Myproj.Algebra.id

Opening Namespaces

To avoid repeated qualification, you can open a namespace:

open Myproj.Algebra

Now id can be used directly.

A more controlled form:

open Myproj.Algebra (id)

This imports only selected names.

Local opening inside a section:

section
  open Myproj.Algebra
  -- local usage
end

This avoids polluting the global scope.

Sections and Variables

Sections allow local parameters:

section

variable (α : Type)

def identity (x : α) := x

end

After the section, identity becomes:

identity : {α : Type} -> α -> α

The variable is generalized into an implicit argument.

This mechanism reduces boilerplate and keeps definitions abstract.

Name Resolution

Lean resolves names using:

1. local context
2. opened namespaces
3. imported modules

Ambiguity is resolved by qualification:

Myproj.Algebra.id

You can inspect names with:

#check Myproj.Algebra.id

If resolution fails, the usual causes are:

• missing import
• namespace not opened
• incorrect module path

Aliases and Renaming

You can introduce shorter names:

namespace Alg := Myproj.Algebra

Then:

Alg.id

This is useful in large developments with deep hierarchies.

Module Design Patterns

A stable layout follows these rules:

• one concept per file when possible
• directory structure mirrors conceptual structure
• minimal imports per file
• avoid circular dependencies
• prefer small modules over large ones

Example layout:

Myproj/
├── Data/
│   ├── List.lean
│   └── Tree.lean
├── Algebra/
│   ├── Group.lean
│   └── Ring.lean

Each file defines a module with the same path.

Minimal Working Example

File:

-- Myproj/Utils.lean
namespace Myproj

def inc (n : Nat) : Nat :=
  n + 1

end Myproj

Use:

import Myproj.Utils

#eval Myproj.inc 5

Expected result:

6

Common Pitfalls

If import X.Y fails, check that the file is X/Y.lean.

If a name is not found, verify the namespace and imports.

If two modules define the same name, avoid open or use qualified names.

If definitions unexpectedly gain implicit arguments, inspect sections and variables.

If imports create cycles, refactor into smaller modules.

Takeaway

Files define modules, and modules define the compilation structure. Namespaces organize declarations and control visibility. A consistent mapping between directories, modules, and namespaces eliminates ambiguity and supports scalable development.