Types and Terms

Everything Has a Type

In Lean, every expression has a type. Think of types as categories that tell you what kind of thing you're working with:

-- Numbers have types
42 : Nat           -- 42 is a natural number
-5 : Int           -- -5 is an integer
3.14 : Float       -- 3.14 is a floating-point number

-- Functions have types
Nat.add : Nat → Nat → Nat   -- takes two Nats, returns a Nat

-- Propositions have types too
(2 + 2 = 4) : Prop   -- this is a proposition

The notation x : T means "x has type T".

The Type Hierarchy

Lean has a hierarchy of "universes" that organize types:

Function Types

The arrow → builds function types:

-- A function from Nat to Nat
def double : Nat → Nat :=
  fun n => n * 2

-- A function taking two arguments
def add : Nat → Nat → Nat :=
  fun a b => a + b

-- Equivalent to:
def add' (a b : Nat) : Nat := a + b

Read Nat → Nat → Nat as "takes a Nat, then another Nat, returns a Nat". The arrows associate to the right: A → B → C means A → (B → C).

Dependent Types

Lean's secret weapon: types can depend on values. This is what makes formal mathematics possible.

-- A vector of exactly n elements
inductive Vec (α : Type) : Nat → Type where
  | nil  : Vec α 0                        -- empty vector has length 0
  | cons : α → Vec α n → Vec α (n + 1)   -- adding element increases length

-- The type Vec α n depends on the value n!
-- Vec Nat 3 is different from Vec Nat 5

With dependent types, the compiler can verify that you never access an out-of-bounds index—the type system catches it!

Structures

Structures bundle related data together:

structure Point where
  x : Float
  y : Float

-- Create a point
def origin : Point := { x := 0.0, y := 0.0 }

-- Or using constructor syntax
def origin' : Point := Point.mk 0.0 0.0

-- Access fields
#check origin.x  -- Float

In cryptography, we use structures to define schemes (commitment schemes, encryption schemes) that bundle operations with their required properties.

Inductive Types

Inductive types define data by listing how to construct it:

-- Natural numbers: either zero or successor of another Nat
inductive Nat where
  | zero : Nat
  | succ : Nat → Nat

-- A list is either empty or an element followed by a list
inductive List (α : Type) where
  | nil  : List α
  | cons : α → List α → List α

-- Boolean: true or false
inductive Bool where
  | false : Bool
  | true  : Bool

Each constructor is a way to build a value of that type. Pattern matching lets us handle each case.

Next Steps

Now you understand Lean's type system. Next, learn how proofs work: