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.

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"[0]!                 -- 'L'
9
10-- String interpolation
11def name := "Lean"
12#eval s!"Hello, {name}!"         -- "Hello, Lean!"

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".split (· == ' ')  -- ["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".containsSubstr "ell"    -- true
9
10-- Transforming
11#eval "hello".toUpper                 -- "HELLO"
12#eval "HELLO".toLower                 -- "hello"
13#eval "  hello  ".trim                -- "hello"
14#eval "hello".replace "l" "L"         -- "heLLo"
15
16-- Substrings
17#eval "hello".take 3                  -- "hel"
18#eval "hello".drop 2                  -- "llo"
19#eval "hello".takeWhile (· != 'l')    -- "he"

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