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.

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	()

The Environment Next: Functions & Definitions