Basic Types

Lean has rich, precise types. This level covers the types you will reach for in every program — and the handful of surprises that trip up newcomers coming from Python, JavaScript, or C.

Learning Goals

• Name and use the core primitive types: Nat, Int, Bool, String, Char.
• Explain why 3 - 5 is 0 in Nat and why that is a feature, not a bug.
• Use type ascription to tell Lean which type you meant.
• Model “might be missing” with Option instead of null.
• Combine values with lists and tuples.

Core Primitive Types

Every value in Lean has exactly one type, and you can always ask what it is with #check. Notice that the types themselves have a type — Type. That is not a curiosity; it is the foundation that makes Lean's proof language work, and you will meet it again in Level 5.

1#check Nat      -- Nat : Type      unbounded non-negative integers
2#check Int      -- Int : Type      positive and negative integers
3#check Bool     -- Bool : Type     true / false
4#check String   -- String : Type   text
5#check Char     -- Char : Type     a single Unicode character
6#check Float    -- Float : Type    64-bit floating point

Nat is not a machine integer

In most languages an integer silently wraps or overflows once it exceeds 64 bits. Lean's Nat is arbitrary precision: it simply keeps counting. Lean uses fast machine arithmetic behind the scenes and switches to big integers when needed, so you get correctness without thinking about it.

1#eval 2 ^ 100
2-- 1267650600228229401496703205376
3
4#eval (2 : Nat) ^ 64
5-- 18446744073709551616   (no overflow, no wraparound)

The Nat Subtraction Surprise

This is the single most common stumbling block for newcomers, so it is worth meeting it early and deliberately. Nat contains only non-negative whole numbers. There is no -2 in Nat to return, so subtraction that would go below zero is truncated to zero.

1#eval 3 - 5          -- 0     ← truncated subtraction on Nat
2#eval (3 : Int) - 5  -- -2    ← ordinary subtraction on Int
3
4#eval 7 / 2          -- 3     ← integer division also truncates
5#eval 7 % 2          -- 1

Type Ascription: Telling Lean What You Meant

A bare numeral like 5 is ambiguous — it could be a Nat, an Int, a Float, or any other numeric type. Lean defaults to Nat when it has nothing else to go on. Write (expr : Type) to override that default.

1#eval (3 - 5 : Nat)  -- 0
2#eval (3 - 5 : Int)  -- -2
3
4-- Same characters, different answer. The type is part of the meaning.

Booleans and Comparison

Bool has exactly two values. Note that equality on values is written == (double equals) and produces a Bool. A single =means something different and more interesting — it builds a proposition, which is the subject of Level 5.

1#eval true && false  -- false   and
2#eval true || false  -- true    or
3#eval !true          -- false   not
4
5#eval 3 == 3         -- true    Bool-valued equality
6#eval 3 < 5          -- true

Strings and Characters

Strings are concatenated with ++. Most string operations are reached with dot notation, which works because they live in the String namespace — "Lean".length is shorthand for String.length "Lean".

1#eval "Lean" ++ " 4"   -- "Lean 4"
2#eval "Lean".length    -- 4
3#eval "Lean".toUpper   -- "LEAN"
4
5#eval 'L'              -- 'L'      single quotes make a Char
6#eval 'L'.toLower      -- 'l'
7
8-- String interpolation: prefix with s! and embed with braces
9#eval s!"2 + 2 = {2 + 2}"   -- "2 + 2 = 4"

Lists

A List αis an ordered, homogeneous collection — every element must have the same type. Lists are built from two pieces: the empty list [], and x :: xs(“cons”) which prepends one element to an existing list. The bracket notation is just sugar for a chain of cons.

1#check List Nat        -- List Nat : Type
2
3#eval [1, 2, 3]        -- [1, 2, 3]
4#eval 0 :: [1, 2, 3]   -- [0, 1, 2, 3]   prepend
5#eval [1, 2] ++ [3]    -- [1, 2, 3]      append
6#eval [1, 2, 3].length -- 3
7#eval [1, 2, 3].reverse -- [3, 2, 1]
8
9-- An empty list needs an ascription: Lean cannot guess the element type
10#eval ([] : List Nat)  -- []

Option: Lean's Answer to Null

What should [10, 20, 30][7] return? There is no seventh element. Most languages answer with null, an exception, or undefined behaviour. Lean answers with a type: Option α is either some x or none, and the type system forces you to say what you want to happen in the none case.

1#eval [10, 20, 30][1]?   -- some 20
2#eval [10, 20, 30][7]?   -- none      no crash, no null
3
4#eval (some 5).getD 0            -- 5     getD = "get with default"
5#eval (none : Option Nat).getD 0 -- 0

The payoff is that a missing value can never surprise you at runtime. If a function returns Option Nat and you try to use it as a Nat, the program does not compile. The bug is caught while you type rather than in production.

Tuples

When you want to return two things at once and they do not deserve a named type yet, use a product. Nat × String is the type of pairs; access the parts with .1 and .2. (When the pair does deserve a name, promote it to a structure — that is Level 4.)

1#check Nat × String    -- Nat × String : Type
2
3#eval (1, "one")       -- (1, "one")
4#eval (1, "one").1     -- 1
5#eval (1, "one").2     -- "one"

Practice

1def safeDiv (x y : Nat) : Option Nat :=
2  if y = 0 then none else some (x / y)
3
4#eval safeDiv 10 2   -- some 5
5#eval safeDiv 10 0   -- none

1def safeSub (x y : Nat) : Option Nat :=
2  if x < y then none else some (x - y)
3
4#eval safeSub 10 3   -- some 7
5#eval safeSub 3 10   -- none

1def describe (xs : List Nat) : String × Nat :=
2  (if xs.isEmpty then "empty" else "non-empty", xs.length)
3
4#eval describe [1, 2, 3]   -- ("non-empty", 3)
5#eval describe []          -- ("empty", 0)

Common Mistakes

• Expecting a negative result from Nat. If a subtraction gives 0 unexpectedly, you are in Nat. Ascribe to Int.
• Writing = where you meant ==. In a Bool position you usually want ==.
• Forgetting the ascription on an empty list. #eval [] fails because Lean cannot infer the element type.
• Trying to use an Option Nat as a Nat. Unwrap it with .getD or a match (Level 6).

Check Yourself

Before moving on, make sure you can answer these without scrolling up:

• What does #eval 2 - 9 print, and why?
• How do you make it print -7 instead?
• What is the difference between [10, 20][5] and [10, 20][5]??
• Why does #eval ([] : List Nat) need the ascription?