Lean4
LanguageTacticsCourse
Module 6 · Lesson 2

Modules & Imports

Organize code into modules for reusability and maintainability. Control what's exported and how it's imported.

File = Module

Each .lean file is a module. The file path determines the module name:

text
1MyProject/
2├── MyProject.lean         -- Module: MyProject
3├── MyProject/
4│   ├── Utils.lean         -- Module: MyProject.Utils
5│   ├── Utils/
6│   │   └── String.lean    -- Module: MyProject.Utils.String
7│   └── Core.lean          -- Module: MyProject.Core

Importing Modules

lean
1-- Import entire module
2import MyProject.Utils
3
4-- Import brings all public definitions into scope
5-- You can now use: Utils.helper, Utils.Config, etc.
6
7-- Import multiple modules
8import MyProject.Utils
9import MyProject.Core
ℹ
Imports are transitive: if A imports B and B imports C, then A has access to C's public definitions.

Namespaces

Group related definitions under a name:

lean
1namespace Math
2
3def square (x : Nat) : Nat := x * x
4def cube (x : Nat) : Nat := x * x * x
5
6end Math
7
8-- Use with qualified name
9#eval Math.square 5   -- 25
10#eval Math.cube 3     -- 27

Opening Namespaces

lean
1-- Open brings names into scope
2open Math
3
4#eval square 5  -- No Math. prefix needed
5
6-- Open temporarily in expression
7#eval (open Math in square 5)
8
9-- Open specific names only
10open Math (square)
11#eval square 5   -- Works
12-- #eval cube 3  -- Error: not in scope

Sections

Sections scope variables and attributes:

lean
1section VectorOps
2  variable (n : Nat)  -- Available in this section
3  
4  def zeros : List Nat := List.replicate n 0
5  def ones : List Nat := List.replicate n 1
6  
7end VectorOps
8
9-- n is no longer in scope here
10#eval zeros 5   -- [0, 0, 0, 0, 0]
Key Takeaway
Namespaces organize names. Sections scope variables andattributes. Often used together for clean module design.

Export and Visibility

Control what's visible outside your module:

lean
1-- Private: only visible in this file
2private def helper (x : Nat) : Nat := x + 1
3
4-- Protected: visible with namespace prefix
5protected def Config.default : Config := ⟨0, ""⟩
6
7-- Public (default): visible everywhere
8def publicFunc : Nat := 42

Re-exporting

lean
1-- In MyProject/Prelude.lean
2import MyProject.Utils
3import MyProject.Core
4
5-- Re-export so users only need one import
6export MyProject.Utils (helper Config)
7export MyProject.Core (main)
lean
1-- Users just import Prelude
2import MyProject.Prelude
3
4-- Gets helper, Config, and main

Module Initialization

Code at the top level runs when the module loads:

lean
1-- This runs when module is imported
2#check "Module loaded"
3
4-- Use initialize for side effects
5initialize : IO Unit := do
6  IO.println "Initializing MyModule..."
7
8-- Register attributes, extensions, etc.
9initialize myExtension : EnvExtension Nat ← 
10  registerEnvExtension (pure 0)

Mutual Dependencies

Lean doesn't allow circular imports. Structure your code to avoid them:

lean
1-- Bad: A imports B, B imports A
2-- This won't compile
3
4-- Good: extract shared code to a third module
5-- Common.lean - shared definitions
6-- A.lean - imports Common
7-- B.lean - imports Common
Deep Dive: Prelude and Init

Every Lean file implicitly imports the Prelude, which provides basic types and functions:

lean
1-- These are available without import:
2-- Nat, Int, Bool, String, List, Option, etc.
3
4-- To write a file without Prelude:
5prelude  -- Must be first line

The prelude directive is used when defining the Prelude itself or for specialized low-level code.

Common Patterns

Barrel File

lean
1-- MyProject.lean (root module)
2-- Re-exports everything for easy importing
3
4import MyProject.Types
5import MyProject.Utils
6import MyProject.Core
7
8export MyProject.Types
9export MyProject.Utils  
10export MyProject.Core

Internal Module

lean
1-- MyProject/Internal.lean
2-- Implementation details not for public use
3
4private def internalHelper := ...
5private structure InternalState := ...
6
7-- Only export what's needed by other internal modules

Feature Modules

lean
1-- Each feature in its own namespace
2-- MyProject/Feature/Auth.lean
3namespace MyProject.Feature.Auth
4  def login := ...
5  def logout := ...
6end MyProject.Feature.Auth
7
8-- MyProject/Feature/Data.lean  
9namespace MyProject.Feature.Data
10  def load := ...
11  def save := ...
12end MyProject.Feature.Data

Best Practices

  • One concept per module: Keep modules focused
  • Match file and namespace: MyProject/Utils.leandefines MyProject.Utils
  • Use private for internals: Don't expose implementation details
  • Provide a root module: Re-export the public API
  • Avoid deep nesting: 3-4 levels maximum
Lake Build SystemNext: Compiling Executables