Module 1 · Level 2

Basic Types

Lean has rich, precise types. This level focuses on the everyday types you will use in every program.

Core Primitive Types

lean

1#check Nat
2#check Int
3#check Bool
4#check String

Lists are ordered collections of values. Option represents a value that might be missing.

lean

1#check List Nat
2#check Option String
3
4#eval ([1, 2, 3] : List Nat)
5#eval (none : Option String)
6#eval (some "Lean" : Option String)

Exercise: Safe Division

Define a function that returns none when dividing by zero andsome otherwise. Then test it with #eval.

lean

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

ℹ

Option is Lean's way to avoid nulls. It forces you to handle missing data explicitly.

Key Takeaway

Types are a feature. The more precise your types, the more help Lean can give you.