Module 1 · Lesson 2

Primitives & Basic Types

Lean 4 has a carefully designed type system. Understanding its basic types—especially why Nat is the default for numbers—is essential.

Natural Numbers (Nat)

In most languages, integer literals like 42 become 32-bit or 64-bit integers. In Lean, they become Nat—natural numbers with arbitrary precision.

lean

1#check 42         -- Nat
2#check 0          -- Nat
3#check 999999999  -- Nat (no overflow!)
4
5#eval 2 ^ 100     -- Works perfectly
6-- 1267650600228229401496703205376

Why Nat? Because natural numbers are mathematically clean. They have no negative values, no overflow, and are perfect for reasoning and proofs. This makes Lean suitable for both programming and mathematics.

Deep Dive: Fixed-Width Integers

When you need fixed-width integers for performance or interoperability, Lean provides:

lean

1#check (42 : UInt8)   -- 8-bit unsigned
2#check (42 : UInt32)  -- 32-bit unsigned  
3#check (42 : UInt64)  -- 64-bit unsigned
4#check (42 : Int32)   -- 32-bit signed
5#check (42 : Int64)   -- 64-bit signed
6
7-- These can overflow!
8#eval (255 : UInt8) + 1  -- 0 (wraps around)

Use fixed-width types only when necessary (e.g., interfacing with C code or specific binary formats).

Integers (Int)

When you need negative numbers, use Int. Unlike Nat, integers include negative values.

lean

1#check (-5 : Int)      -- Int
2#check (42 : Int)      -- Int (explicit cast)
3
4#eval (-10 : Int) + 3  -- -7
5#eval (5 : Int) - 10   -- -5
6
7-- Warning: Nat subtraction saturates at 0!
8#eval 5 - 10           -- 0 (because this is Nat)

⚠

Subtraction on Nat never goes negative—it saturates at zero. If you need negative results, cast to Int first.

Total Arithmetic: Division and Modulo

Lean has no exceptions and no undefined behaviour in pure code: every function must return a value for every input. That forces a decision about division by zero, and Lean's answer surprises newcomers.

lean

1-- Division truncates toward zero on Nat
2#eval 7 / 2            -- 3
3#eval 7 % 2            -- 1
4
5-- Division by zero is DEFINED, and equals zero
6#eval (5 : Nat) / 0    -- 0
7#eval (5 : Nat) % 0    -- 5
8
9-- This is a definitional truth you can prove by rfl
10example : (5 : Nat) / 0 = 0 := rfl
11
12-- On Int, / rounds toward negative infinity, and % follows it
13#eval (-7 : Int) / 2   -- -4
14#eval (-7 : Int) % 2   -- 1

ℹ

x / 0 = 0 is not a bug or a silent failure — it is a deliberate choice that keeps division a total function. The cost is that a theorem like a / b * b = a needs the hypothesis b ≠ 0 explicitly; the benefit is that you never have to prove a divisor is nonzero just to write a division.

Coercions Between Numeric Types

Lean inserts conversions automatically when the expected type is known. The up-arrow ↑ you see in the goal display is exactly that insertion made visible.

lean

1def n : Nat := 3
2
3-- Nat → Int happens silently, shown as ↑n
4#check (n : Int)       -- ↑n : Int
5#eval  (n : Int) - 10  -- -7   (no saturation: this is Int subtraction)
6
7-- Nat → Float is explicit
8#eval (3 : Nat).toFloat  -- 3.000000
9
10-- WHERE the coercion lands changes the answer:
11def a : Nat := 3
12def b : Nat := 10
13
14#eval (a - b : Int)      -- -7 : Lean coerces the OPERANDS, so this is Int subtraction
15#eval ((a - b : Nat) : Int)  -- 0 : Nat subtraction saturated first, then coerced

⚠

This is the most common numeric surprise in Lean. Modern Lean is helpful here: an ascription like (a - b : Int) pushes the coercioninward onto a and b, so you get real integer subtraction. But as soon as the subtraction is pinned to Nat by something else — a helper function that returns Nat, or an explicit (… : Nat) — it saturates at zero and the later coercion cannot recover the lost information.

lean

1-- The trap in the wild: the Nat is fixed by the function's return type
2def diff (x y : Nat) : Nat := x - y
3
4#eval (diff 3 10 : Int)   -- 0, NOT -7 — the clamping already happened inside diff
5
6-- Fix: make the function return Int, and coerce at the boundary
7def diff' (x y : Nat) : Int := (x : Int) - y
8#eval diff' 3 10          -- -7

Bool vs Prop

Comparisons look like they return Bool, but they do not. 5 > 3 is a Prop — a statement — and Lean turns it into a Bool only when a Decidable instance says how to compute it.

lean

1#check 5 > 3           -- 5 > 3 : Prop      (a statement, not a value)
2#eval  5 > 3           -- true              (decided, then evaluated)
3
4-- decide turns a decidable Prop into the Bool that witnesses it
5#eval decide (5 > 3)   -- true
6
7-- == is the Bool-valued equality test (BEq); = is the Prop
8#check "a" == "b"      -- Bool
9#check "a" = "b"       -- Prop
10
11-- if-then-else accepts either, because it takes a Decidable condition
12#eval if 5 > 3 then "yes" else "no"   -- "yes"

💡

Keep the distinction in mind from day one: Prop is what you prove, Bool is what you compute. Mixing them up is the source of most "type mismatch: expected Bool, got Prop" errors. The Tactics track covers this in depth.

Floating-Point Numbers (Float)

For decimal numbers, Lean uses 64-bit IEEE 754 floating-point:

lean

1#check 3.14       -- Float
2#check 2.5e10     -- Float (scientific notation)
3
4#eval 3.14 * 2.0  -- 6.280000
5#eval 1.0 / 3.0   -- 0.333333...

Booleans (Bool)

Booleans in Lean are exactly what you expect:

lean

1#check true   -- Bool
2#check false  -- Bool
3
4-- Boolean operations
5#eval true && false   -- false (and)
6#eval true || false   -- true (or)
7#eval !true           -- false (not)
8
9-- Comparison returns Bool
10#eval 5 > 3           -- true
11#eval "a" == "b"      -- false

Characters and Strings

Char represents a single Unicode code point. String is a sequence of characters.

lean

1#check 'a'        -- Char
2#check '∀'        -- Char (Unicode works!)
3#check "Hello"    -- String
4
5-- String operations
6#eval "Hello" ++ " " ++ "World"  -- "Hello World"
7#eval String.length "Lean"       -- 4
8#eval "Lean".front               -- 'L'  (first character)
9#eval "Lean".toList              -- ['L', 'e', 'a', 'n']
10
11-- String interpolation
12def name := "Lean"
13#eval s!"Hello, {name}!"         -- "Hello, Lean!"

⚠

A String is not an array of characters, and s[i] with a Nat does not compile. Lean stores strings as UTF-8, so a character position is a String.Pos (a byte offset), not an index. Indexing by character number is O(n) — if you need random access, convert once with .toList or .toArray and index that.

Key Takeaway

The s!"..." syntax enables string interpolation. Curly braces{expr} insert the value of any expression.

More String Operations

Strings have many useful methods for text processing:

lean

1-- Splitting and joining
2#eval "hello world".splitOn " "       -- ["hello", "world"]
3#eval " ".intercalate ["a", "b", "c"] -- "a b c"
4
5-- Searching
6#eval "hello".startsWith "he"         -- true
7#eval "hello".endsWith "lo"           -- true
8#eval "hello".contains "ell"          -- true  (substring)
9#eval "hello".contains 'e'            -- true  (single character)
10
11-- Transforming
12#eval "hello".toUpper                 -- "HELLO"
13#eval "HELLO".toLower                 -- "hello"
14#eval "  hello  ".trimAscii           -- hello  (a Slice — see the note below)
15#eval "hello".replace "l" "L"         -- "heLLo"
16
17-- Substrings. Note: take/drop/takeWhile return a String.Slice — a cheap
18-- view into the original string, not a copy. Add .toString if you need a
19-- real String back.
20#eval "hello".take 3                  -- hel
21#eval ("hello".take 3).toString       -- "hel"
22#eval "hello".drop 2                  -- llo
23#eval "hello".takeWhile (· != 'l')    -- he

ℹ

The String API has been actively reworked across recent Lean releases (slices, trimAscii, String.Pos.Raw). If a name here does not resolve in your toolchain, hover it in the editor — Lean's deprecation warnings tell you the current name. The examples above are checked against Lean 4.32.

Bounded Naturals (Fin n)

Fin n represents natural numbers less than n. This is crucial for safe array indexing where you can prove the index is in bounds.

lean

1-- Fin n: numbers 0, 1, ..., n-1
2#check (⟨2, by omega⟩ : Fin 5)  -- A number < 5
3
4-- Safe array indexing with Fin
5def arr : Array String := #["a", "b", "c"]
6def safeGet (arr : Array α) (i : Fin arr.size) : α := arr[i]
7
8-- The type system ensures i is always valid
9-- No runtime bounds checking needed!
10
11-- Creating Fin values
12#eval (3 : Fin 10)        -- 3
13#eval (0 : Fin 5)         -- 0
14
15-- Fin arithmetic wraps around
16#eval (4 : Fin 5) + 1     -- 0 (wraps)

ℹ

Fin n is how Lean achieves safe array access. When you use arr[i] with a Fin arr.size, the compiler knows the access is always valid.

Numeric Literal Type Inference

Numeric literals like 42 are polymorphic—their type depends on context:

lean

1-- Type inferred from usage
2def natVal := 42          -- Inferred as Nat (default)
3def intVal : Int := 42    -- Int, because we said so
4def floatVal : Float := 42-- Float, coerced from literal
5
6-- Context determines type
7def needsInt (x : Int) : Int := x * 2
8#eval needsInt 42         -- 42 is treated as Int here
9
10-- Explicit type ascription
11#eval (42 : UInt8)        -- 42 as 8-bit unsigned
12#eval (42 : Int32)        -- 42 as 32-bit signed
13
14-- Default is always Nat
15#check 42                 -- Nat

Choosing the Right Numeric Type

A good rule of thumb: use Nat for counts and sizes, Intfor values that can go negative, and fixed-width integers only when you need binary compatibility or performance constraints.

Nat: sizes, lengths, indices, and proof-friendly arithmetic.
Int: balances, offsets, or any signed values.
UInt8/UInt32: file formats, bit-level operations, C interop.

The Unit Type

Unit is a type with exactly one value: (). It's used when a function doesn't need to return meaningful data.

lean

1#check ()     -- Unit
2#check Unit   -- Type
3
4-- A function that "returns nothing"
5def printHello : IO Unit := IO.println "Hello"

Type Annotations

You can explicitly specify types using the colon syntax:

lean

1-- Explicit type annotations
2def x : Nat := 42
3def y : Int := -5
4def z : Float := 3.14
5
6-- In expressions
7#eval (42 : Int) - 100  -- -58
8
9-- Type ascription in complex expressions
10def result := ((5 : Int) - 10) * 2  -- -10

Type Summary

Type	Description	Examples
Nat	Arbitrary-precision natural numbers	0, 42, 2^100
Int	Arbitrary-precision integers	-5, 0, 42
Float	64-bit floating point	3.14, 2.5e10
Bool	Boolean values	true, false
Char	Unicode character	'a', '∀'
String	Text string	"Hello"
Unit	Single value type	()

Exercise: Cast and Compute

Create a Nat and an Int with the same literal. Then subtract 10 from both and compare the results.

lean

1def n : Nat := 5
2def i : Int := 5
3
4#eval n - 10      -- What happens?
5#eval i - 10      -- What happens?

The Environment Next: Functions & Definitions