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

The importstatement makes another module's definitions available. All public definitions from the imported module become accessible.

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.

Selective Imports

You can import a module but open only specific names to keep your namespace clean.

lean

1import MyProject.Utils
2
3-- Open only a few definitions
4open MyProject.Utils (Config defaultConfig)
5
6-- Other names remain qualified
7-- #check helper  -- not in scope unless opened

Namespaces

Namespaces group related definitions under a common prefix. This prevents name collisions and makes code organization explicit.

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

Opening a namespace brings its definitions into scope without requiring the full prefix. You can open temporarily for one expression or for the rest of the file.

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

initialize registers an IO action to run once, when the module is first loaded — before any code that imports it. This is how libraries register attributes, tactics, and global state.

lean

1-- Run an action at load time. Note: no ":" and no type after initialize.
2initialize do
3  IO.println "Initializing MyModule..."
4
5-- Bind the result to a name with ← : the classic use is a global reference
6initialize counterRef : IO.Ref Nat ← IO.mkRef 0
7
8-- Register an environment extension (how attributes are implemented)
9initialize myExtension : EnvExtension Nat ←
10  registerEnvExtension (pure 0)

⚠

Two traps. First, the syntax is initialize do … — writing initialize : IO Unit := do is a parse error. Second, a name introduced by initialize cannot be #eval'd in the same file: Lean reports cannot evaluate [init] declaration in the same module, because the initializer has not run yet while that file is being elaborated. Use it from an importing module.

ℹ

Ordinary top-level commands like #check and #eval do not run on import. They run once, when their own file is elaborated, and leave nothing behind but their output in the infoview. Only initialize gives you load-time behaviour.

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-- One import for users, instead of five
3
4import MyProject.Types
5import MyProject.Utils
6import MyProject.Core
7
8-- Note: "export Ns" alone is a parse error. export always takes a
9-- parenthesised list of names.
10export MyProject.Types (Config Status)
11export MyProject.Utils (helper format)
12export MyProject.Core (run)

Internal Module

lean

1-- MyProject/Internal.lean
2-- Implementation details not for public use
3
4private def internalHelper (n : Nat) : Nat := n * 2
5
6private structure InternalState where
7  cache : List Nat
8  dirty : Bool
9
10-- private means "not visible outside THIS FILE" - not "outside this
11-- namespace". An importing module cannot see either of the above,
12-- even fully qualified.

Feature Modules

lean

1-- Each feature in its own namespace
2-- MyProject/Feature/Auth.lean
3namespace MyProject.Feature.Auth
4  def login (user : String) : Bool := user != ""
5  def logout : Unit := ()
6end MyProject.Feature.Auth
7
8-- MyProject/Feature/Data.lean
9namespace MyProject.Feature.Data
10  def load (path : String) : IO String := IO.FS.readFile path
11  def save (path content : String) : IO Unit := IO.FS.writeFile path content
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

Exercise: Create a Namespace

Define two functions in a namespace and call them with and without open.

lean

1namespace Strings
2def shout (s : String) : String := s.toUpper
3def whisper (s : String) : String := s.toLower
4end Strings
5
6#eval Strings.shout "Lean"
7
8open Strings
9#eval whisper "LEAN"

Lake Build System Next: Compiling Executables