Lean 4 Syntax: Declarations, Namespaces, and Modules

Lean 4’s surface syntax is expressive and whitespace-sensitive. Every source file is a module, declarations are organized into namespaces, and the universe system lets you write polymorphic definitions that work at any type level. This page introduces the structural building blocks of every Lean 4 file — the syntax you will encounter before any logic or proofs.

Source Files and Modules

Every .lean file is a module. The module name corresponds to the file path relative to the package root (with / replaced by . and the .lean extension removed). A file at MyPkg/Data/List.lean defines the module MyPkg.Data.List.

Import Statements

import statements must appear at the very top of a file (before any declarations). They bring another module’s public declarations into scope:

import Std.Data.HashMap
import MyPkg.Data.List

Lean’s standard library (Init) is imported automatically by default. To suppress this and start from scratch, use the prelude keyword:

-- Only for advanced use (e.g., when writing Init itself)
prelude
import Init.Core

In ordinary Lean files (those without an explicit module keyword), import statements are re-exported by default, so transitive imports are visible. In files that begin with the module keyword, only public import statements are re-exported; bare import statements are private to that module.

Comments

-- This is a single-line comment

/-
  This is a block comment.
  It can span multiple lines.
-/

/--
  This is a **doc-string comment**.
  It must immediately precede a declaration and is rendered by the LSP
  and by `#check`.
-/
def myFunction := 42

Declarations

The top-level commands that add definitions to the environment:

-- Constant definition
def answer : Nat := 42

-- A theorem (proof term)
theorem one_plus_one : 1 + 1 = 2 := rfl

-- An abbreviation (always unfolded by the elaborator)
abbrev MyNat := Nat

-- A noncomputable definition (cannot be executed, but can be reasoned about)
-- (Classical.choice requires a nonemptiness proof and cannot be executed)
noncomputable def someNat : Nat := Classical.choice ⟨0⟩

Whitespace Sensitivity

Lean 4 uses indentation to delimit blocks. A do block, match arms, where clauses, and tactic blocks all use indentation rather than explicit delimiters (though curly braces with semicolons are also accepted):

def classify (n : Nat) : String :=
  match n with
  | 0 => "zero"
  | 1 => "one"
  | _ => "many"

def countdown (n : Nat) : IO Unit := do
  let mut i := n
  while i > 0 do
    IO.println s!"T minus {i}"
    i := i - 1
  IO.println "Liftoff!"

Namespaces

Namespaces group related declarations and avoid name collisions.

namespace Geometry

def pi : Float := 3.141592653589793

def circleArea (r : Float) : Float := pi * r * r

namespace Circle
  def circumference (r : Float) : Float := 2 * pi * r
end Circle

end Geometry

-- Access with fully-qualified name
#eval Geometry.pi                   -- 3.141592653589793
#eval Geometry.Circle.circumference 1.0  -- 6.283185307179586

Opening Namespaces

open brings names from a namespace into scope without full qualification:

open Geometry in
#eval circleArea 3.0   -- works only in the scope of this `open`

-- Persistent open for the rest of the file (or until `end`)
open Geometry
#eval pi               -- 3.141592653589793

You can also open selectively:

open Nat (succ zero) in
#eval succ (succ zero)  -- 2

Sections and `variable`

Sections let you declare shared parameters once instead of repeating them on every definition:

section MySection

variable (α : Type*) [BEq α] [Hashable α]

def countOccurrences (xs : List α) (target : α) : Nat :=
  xs.foldl (fun acc x => if x == target then acc + 1 else acc) 0

-- α, BEq, and Hashable are automatically added as arguments
end MySection

The variable command declares parameters that are automatically included as implicit or instance arguments on any definition in the current scope that mentions them.

Universe Polymorphism

Lean’s type hierarchy is: Sort 0 = Prop, Sort 1 = Type = Type 0, Sort 2 = Type 1, … You can write universe-polymorphic definitions using universe variables:

universe u v

-- Works for any universe level
def myId {α : Sort u} (a : α) : α := a

-- Explicit universe annotation
def myPair {α : Type u} {β : Type v} (a : α) (b : β) : α × β := (a, b)

The shorthand Type* (or Type _) lets Lean infer the universe level:

def identity {α : Type*} (a : α) : α := a

Attributes

Attributes annotate declarations with metadata that affects elaboration, simplification, or code generation:

-- Mark as a simp lemma (used by the simp tactic automatically)
@[simp]
theorem add_zero_eq (n : Nat) : n + 0 = n := by simp

-- Inline the function at call sites
@[inline]
def fastAdd (a b : Nat) : Nat := a + b

-- Expose to C under the given symbol name
@[extern "my_c_function"]
opaque myFunction : Nat → Nat

-- Mark as reducible (unfolded at reducible transparency)
@[reducible]
def MyAlias := Nat × Nat

Multiple attributes can be combined:

@[simp, inline]
theorem mul_one (n : Nat) : n * 1 = n := by simp

Query Commands

These commands query the current environment and are invaluable during development:

`#check`

Displays the type of an expression:

#check Nat.add          -- Nat.add : Nat → Nat → Nat
#check (· + 1)          -- fun x => x + 1 : Nat → Nat
#check @List.map        -- @List.map : {α β : Type u_1} → (α → β) → List α → List β

`#eval`

Evaluates an expression and prints the result:

#eval 2 ^ 10            -- 1024
#eval "Hello".length    -- 5
#eval List.range 5      -- [0, 1, 2, 3, 4]

`#print`

Prints the full definition of a declaration, including its type and body:

#print Nat.add
-- def Nat.add : Nat → Nat → Nat := ...

#print axioms Nat.rec
-- Nat.rec depends on no axioms

Use #check @foo (with @) to see all arguments including implicit ones. Use #print axioms myTheorem to verify a proof is axiom-free (or to see which axioms it depends on, such as Classical.choice or propext).

`set_option`

Lean’s behaviour can be tuned with set_option:

-- Show implicit arguments in displayed types
set_option pp.all true in
#check List.map

-- Enable/disable a linter locally
set_option linter.unusedVariables false in
def foo (x : Nat) : Nat := 0

Summary of Key Syntax Elements

Syntax	Purpose
`import Foo.Bar`	Import a module
`namespace Foo … end Foo`	Open a namespace block
`open Foo`	Bring namespace into scope
`section … end`	Delimit a variable scope
`variable (x : α)`	Declare a shared parameter
`universe u`	Declare a universe variable
`@[attr]`	Apply an attribute
`#check e`	Print the type of `e`
`#eval e`	Evaluate and print `e`
`#print name`	Print a declaration’s definition
`-- comment`	Single-line comment
`/- … -/`	Block comment
`/-- … -/`	Doc-string comment

Introduction

Language Basics

Theorem Proving

Functional Programming

Lean 4 Syntax: Declarations, Namespaces, and Modules

Source Files and Modules

Import Statements

Comments

Declarations

Whitespace Sensitivity

Namespaces

Opening Namespaces

Sections and `variable`

Universe Polymorphism

Attributes

Query Commands

`#check`

`#eval`

`#print`

`set_option`

Summary of Key Syntax Elements

Build docs developers (and LLMs) love

Introduction

Language Basics

Theorem Proving

Functional Programming

Documentation Index

​Source Files and Modules

​Import Statements

​Comments

​Declarations

​Whitespace Sensitivity

​Namespaces

​Opening Namespaces

​Sections and variable

​Universe Polymorphism

​Attributes

​Query Commands

​#check

​#eval

​#print

​set_option

​Summary of Key Syntax Elements

Build docs developers (and LLMs) love

Source Files and Modules

Import Statements

Comments

Declarations

Whitespace Sensitivity

Namespaces

Opening Namespaces

Sections and `variable`

Universe Polymorphism

Attributes

Query Commands

`#check`

`#eval`

`#print`

`set_option`

Summary of Key Syntax Elements