Documentation Index
Fetch the complete documentation index at: https://mintlify.com/leanprover/lean4/llms.txt
Use this file to discover all available pages before exploring further.
In Lean 4, every expression has a type and types are themselves first-class expressions. The same core language handles both programs and proofs, because a proof of proposition P is simply a term of type P. This page surveys the type hierarchy, built-in concrete types, compound types, and the expression forms you will use constantly when writing Lean code.
The Universe Hierarchy
Types are organized in a hierarchy of universes:
| Universe | Also written as | Contains |
|---|
Sort 0 | Prop | Propositions (proof-irrelevant) |
Sort 1 | Type or Type 0 | Ordinary data types |
Sort 2 | Type 1 | Types of types |
Sort u | Type (u - 1) | The u-th universe |
#check Prop -- Prop : Type 1 (Sort 0 is a Type itself)
#check Type -- Type : Type 1
#check Type 0 -- Type 0 : Type 1
#check Type 1 -- Type 1 : Type 2
#check Sort 0 -- Sort 0 : Sort 1 (Sort 0 = Prop)
Prop is proof-irrelevant: two proofs of the same proposition are definitionally equal. This makes it safe to erase proofs during compilation.
-- Prop example
example : 1 + 1 = 2 := rfl -- rfl : 1 + 1 = 2
-- Type example
#check (Nat : Type) -- Nat : Type
#check (List Nat : Type) -- List Nat : Type
Universe polymorphism lets you write one definition that works at any level. Use universe u to declare a universe variable, then write Type u in your signature.
Built-in Scalar Types
Nat — Natural Numbers
Nat is the type of non-negative integers (0, 1, 2, …). It is defined as an inductive type in Init.Prelude and given an efficient arbitrary-precision implementation by the compiler:
-- Subtraction on Nat saturates at 0
#eval (5 : Nat) - 3 -- 2
#eval (3 : Nat) - 5 -- 0
-- Nat literals
def x : Nat := 1_000_000
Int — Integers
#eval (3 : Int) - 5 -- -2
#eval Int.natAbs (-7) -- 7
Bool — Booleans
-- Two constructors: Bool.true, Bool.false (exported as true and false)
#eval true && false -- false
#eval !true -- false
#eval (true : Bool) -- true
Char — Unicode Characters
#eval 'A'.toNat -- 65
#eval Char.isAlpha 'z' -- true
String — UTF-8 Strings
#eval "hello".length -- 5
#eval "hello " ++ "world" -- "hello world"
#eval s!"Result: {1 + 1}" -- "Result: 2" (string interpolation)
Float — Double-Precision Floating Point
#eval (3.141592653589793 : Float) -- 3.141592653589793
#eval Float.sqrt 2.0 -- 1.4142135623730951
#eval (2.5 : Float) + 1.0 -- 3.5
Fixed-Width Integer Types
Lean provides UInt8, UInt16, UInt32, UInt64, USize (unsigned) and Int8, Int16, Int32, Int64 (signed):
#eval (255 : UInt8) + 1 -- 0 (wraps around)
#eval (127 : Int8) -- 127
Product Types (Tuples)
The product type α × β (written Prod α β) pairs two values. Tuples are right-nested:
-- Pair
def p : Nat × String := (42, "hello")
#eval p.1 -- 42
#eval p.2 -- "hello"
-- Triple (right-nested pair)
def t : Nat × String × Bool := (1, "yes", true)
#eval t.1 -- 1
#eval t.2.1 -- "yes"
#eval t.2.2 -- true
def p2 : Nat × String := ⟨42, "hello"⟩
Sum Types
The sum type α ⊕ β (written Sum α β) holds either a value of type α or one of type β:
def left : Sum Nat String := Sum.inl 42
def right : Sum Nat String := Sum.inr "hello"
def describe (x : Sum Nat String) : String :=
match x with
| .inl n => s!"Number: {n}"
| .inr s => s!"String: {s}"
#eval describe left -- "Number: 42"
#eval describe right -- "String: hello"
Option — Optional Values
Option α is either some a (containing a value a : α) or none (no value):
def safeDivide (n d : Nat) : Option Nat :=
if d == 0 then none else some (n / d)
#eval safeDivide 10 2 -- some 5
#eval safeDivide 10 0 -- none
-- Pattern matching
def showResult (x : Option Nat) : String :=
match x with
| some n => s!"Got {n}"
| none => "Nothing"
List — Linked Lists
List α is the standard singly-linked list:
def nums : List Nat := [1, 2, 3, 4, 5]
#eval nums.length -- 5
#eval nums.head? -- some 1
#eval nums.tail -- [2, 3, 4, 5]
#eval nums.map (· * 2) -- [2, 4, 6, 8, 10]
#eval nums.filter (· % 2 == 0) -- [2, 4]
#eval nums.foldl (· + ·) 0 -- 15
Array — Dynamic Arrays
Array α provides O(1) random access and amortised O(1) push/pop, unlike the linked List:
def arr : Array Nat := #[10, 20, 30, 40]
#eval arr.size -- 4
#eval arr[0]! -- 10 (panics if out of range)
#eval arr[2]? -- some 30
#eval arr.push 50 -- #[10, 20, 30, 40, 50]
#eval arr.map (· + 1) -- #[11, 21, 31, 41]
-- Safe indexed access with proof
example : arr[1]'(by simp [arr]) = 20 := rfl
Prefer Array over List when you need random access or are appending many elements. Prefer List when you need structural recursion with easy pattern matching on the head.
Type Ascription
Ascription forces an expression to have a particular type:
#check (42 : Int) -- 42 : Int (instead of the default Nat)
#check ([] : List Int) -- [] : List Int
def x := (0 : Float) -- explicitly Float, not Nat
Let Expressions
def example1 : Nat :=
let a := 10
let b := a * 2
a + b -- 30
-- let with type annotation
def example2 : String :=
let n : Nat := 7
let s : String := s!"n = {n}"
s
let mut creates a mutable local variable (only inside do blocks):
def sumList (xs : List Nat) : IO Nat := do
let mut total := 0
for x in xs do
total := total + x
return total
where Clauses
where defines local helper definitions scoped to the enclosing declaration:
def fib (n : Nat) : Nat :=
go n 0 1
where
go : Nat → Nat → Nat → Nat
| 0, a, _ => a
| n + 1, a, b => go n b (a + b)
#eval fib 10 -- 55
Dependent Types
In Lean 4, types can depend on values. The canonical example is Vector α n, a list of exactly n elements:
-- A type whose second argument is a Nat value
inductive Vector (α : Type u) : Nat → Type u where
| nil : Vector α 0
| cons : α → Vector α n → Vector α (n + 1)
def myVec : Vector Nat 3 :=
.cons 1 (.cons 2 (.cons 3 .nil))
-- The type encodes the length: you cannot confuse a length-3 with a length-2 vector
if/else Expressions
def abs (n : Int) : Int :=
if n ≥ 0 then n else -n
-- Dependent if: the branches can use the condition as a proof
def safeHead (xs : List Nat) : Option Nat :=
if h : xs.length > 0 then
some (xs.get ⟨0, h⟩)
else
none
match Expressions
def describeList (xs : List Nat) : String :=
match xs with
| [] => "empty"
| [x] => s!"singleton {x}"
| x :: _ => s!"starts with {x}"
-- Nested patterns
def sumPairs (ps : List (Nat × Nat)) : Nat :=
match ps with
| [] => 0
| (a, b) :: rest => a + b + sumPairs rest
