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

```text
Myproj/Algebra/Group.lean
```

defines the module:

```lean
import Myproj.Algebra.Group
```

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

```lean
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:

```lean
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.

```lean
namespace Myproj

def x : Nat := 1

end Myproj
```

The fully qualified name is:

```lean
Myproj.x
```

Namespaces can be nested:

```lean
namespace Myproj.Algebra

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

end Myproj.Algebra
```

This produces:

```lean
Myproj.Algebra.id
```

## Opening Namespaces

To avoid repeated qualification, you can open a namespace:

```lean
open Myproj.Algebra
```

Now `id` can be used directly.

A more controlled form:

```lean
open Myproj.Algebra (id)
```

This imports only selected names.

Local opening inside a section:

```lean
section
  open Myproj.Algebra
  -- local usage
end
```

This avoids polluting the global scope.

## Sections and Variables

Sections allow local parameters:

```lean
section

variable (α : Type)

def identity (x : α) := x

end
```

After the section, `identity` becomes:

```lean
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:

```lean
Myproj.Algebra.id
```

You can inspect names with:

```lean
#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:

```lean
namespace Alg := Myproj.Algebra
```

Then:

```lean
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:

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

Each file defines a module with the same path.

## Minimal Working Example

File:

```lean
-- Myproj/Utils.lean
namespace Myproj

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

end Myproj
```

Use:

```lean
import Myproj.Utils

#eval Myproj.inc 5
```

Expected result:

```text
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.