Lean by Example

A compact tour of the Lean 4 language, drawn from Chapter 2 of Theorem Proving in Lean 4. Companion to Propositions as Types, Annotated.

The goal of this page is to get you comfortable reading and writing Lean code. It departs from the book's section order and groups related constructs where they belong. The deeper ideas in Chapter 2 (universe hierarchies, what makes dependent type theory dependent, how implicit elaboration actually works) will live in a separate post; this page shows you the syntax you'll type.

Three commands do most of the work when you're exploring Lean:

def m : Nat := 1
#check m
  | m : Nat
#eval m + 2
  | 3

def names a new constant. #check asks Lean for the type of an expression; #eval asks Lean to compute the value. The # prefix is a convention for commands that query the system without adding to it.

Comments come in two forms. Line comments start with --; block comments are delimited by /- and -/ and can be nested.

-- a line comment
/- a block comment
   /- nested block -/
   can be commented-out code -/

The built-in types you'll meet first are Nat, Bool, and String.

#check 0
  | 0 : Nat
#check true
  | true : Bool
#check "hello"
  | "hello" : String

Nat is Lean's type of natural numbers (0, 1, 2, ...)1. Bool has two values, true and false. String is exactly what you'd expect.

You can introduce your own named values of these types with def:

def n : Nat := 42
def greeting : String := "hi"
def ok : Bool := true

Bool has the usual logical operators: && (and), || (or), ! (not).

#eval true && false
  | false
#eval true || false
  | true
#eval !true
  | false

Two type constructors cover most of what you need: → for function types, × for product types. Both take types and return types.

#check Nat → Bool
  | Nat → Bool : Type
#check Nat × Bool
  | Nat × Bool : Type

→ and × are both Unicode; Lean has ASCII fallbacks (-> and no fallback for ×), but in practice you type them directly2.

Both constructors are themselves functions from types to types; you can nest them to build up whatever function signature you need.

#check Nat → Nat → Nat
  | Nat → Nat → Nat : Type
#check (Nat → Nat) → Nat
  | (Nat → Nat) → Nat : Type

Functions apply by juxtaposition: f x, not f(x). Multiple arguments are separated by spaces: Nat.add 3 2.

#check Nat.add
  | Nat.add : Nat → Nat → Nat
#check Nat.add 3
  | Nat.add 3 : Nat → Nat
#check Nat.add 3 2
  | Nat.add 3 2 : Nat
#eval Nat.add 3 2
  | 5

Why does Nat.add have three Nats in its type? Because → is right-associative. Nat → Nat → Nat parses as Nat → (Nat → Nat): a function that takes one Nat and returns a function that takes a Nat and returns a Nat.

That's why you can apply it to one argument at a time. Each application eats one arrow:

This is the difference between a curried function and one that takes a pair. Nat.add could have been written with type Nat × Nat → Nat, taking a single argument of type Nat × Nat. In practice, type theory prefers the curried form because it allows partial application for free.

Pairs have their own syntax. You write (a, b) to construct, and .1 / .2 (or .fst / .snd) to project:

#check (5, 9)
  | (5, 9) : Nat × Nat
#eval (5, 9).1
  | 5
#eval (5, 9).2
  | 9

Anonymous functions use fun, which is synonymous with λ. Both of these are the same expression:

fun x => x + 5
λ x => x + 5

You can annotate the parameter's type, but Lean usually infers it:

#check fun x => x + 5
  | fun x => x + 5 : Nat → Nat
#check fun (x : Nat) => x + 5
  | fun x => x + 5 : Nat → Nat
#eval (fun x => x + 5) 10
  | 15

Multiple parameters are separated by spaces:

#check fun x y => if !y then x + 1 else x + 2
  | fun x y => ... : Nat → Bool → Nat

Applying a lambda to an argument and substituting the argument into the body is called beta reduction. Lean treats the two forms as definitionally equal3: the type checker cannot distinguish (fun x => x + 1) 3 from 4.

A def can take parameters directly, which is how you usually write named functions:

def double (x : Nat) : Nat := x + x

def add (x y : Nat) : Nat := x + y

#eval double 5
  | 10
#eval add 3 4
  | 7

This is shorthand for a def whose value is a fun. The two forms below are equivalent:

def double (x : Nat) : Nat := x + x
def double : Nat → Nat := fun x => x + x

The same arrow-vs.-binder equivalence shows up when reading the type of a built-in like And in Propositions as Types.

You can leave off the return type when Lean can infer it, though writing it out is often clearer:

def double (x : Nat) := x + x  -- return type inferred

Functions can take other functions as arguments:

def doTwice (f : Nat → Nat) (x : Nat) : Nat := f (f x)

#eval doTwice double 2
  | 8

And they can take types as arguments. That lets you write a polymorphic function that works for any type:

def compose (α β γ : Type) (g : β → γ) (f : α → β) (x : α) : γ :=
  g (f x)

A quick word on binder grouping. Parameters that share a type can be merged into one binder: (a b c : Nat) is exactly shorthand for (a : Nat) (b : Nat) (c : Nat). There is no cap on how many names you can pack into a group, and the two forms are interchangeable. compose uses both styles: (α β γ : Type) collapses three same-typed parameters into one group, while g, f, and x each get their own group because their types differ.

Binders read left to right, and a later binder may refer to names introduced by an earlier one. In compose, the type β → γ of g uses names bound by the preceding (α β γ : Type). This order-dependence (a form of dependent typing) is why groups cannot be freely reshuffled.

Passing the type α every time you call compose is verbose. The implicit arguments section shows how Lean can infer it for you.

let names an intermediate value inside an expression:

def twiceDouble (x : Nat) : Nat :=
  let y := x + x
  y * y

#eval twiceDouble 3
  | 36

You can chain multiple lets. A semicolon ; separates them, and line breaks count as semicolons:

def example1 : Nat :=
  let a := 1
  let b := a + 1
  let c := b + 1
  c

A let is inlined, not stored: let a := t1; t2 is definitionally equal to t2 with a replaced by t1.

Every expression in Lean has a type, including types themselves. Nat has type Type. Type has type Type 1. Type 1 has type Type 2. And so on up the hierarchy.

#check Nat
  | Nat : Type
#check Type
  | Type : Type 1
#check Type 1
  | Type 1 : Type 2

Type is short for Type 0. Because types are values, you can name them with def:

def MyNat : Type := Nat

#check MyNat
  | MyNat : Type

The hierarchy exists to avoid paradoxes; the practical consequence is that polymorphic types carry a universe parameter:

#check List
  | List.{u} (α : Type u) : Type u

The .{u} is a universe variable: List works at any level of the hierarchy. You rarely write universe variables explicitly; Lean inserts them for you. The deeper story belongs to another post.

Three constructs control scope and naming.

variable declares an implicit parameter that gets inserted into any subsequent definition that mentions it. This lets you avoid repeating yourself:

variable (α : Type) (f : α → α)

def doTwice (x : α) : α := f (f x)

-- Lean elaborates this as: def doTwice (α : Type) (f : α → α) (x : α) : α := f (f x)

section ... end limits the scope of variable declarations. Variables declared inside the section are only in scope until end:

section
  variable (α : Type) (f : α → α)
  def doTwice (x : α) : α := f (f x)
  def doThrice (x : α) : α := f (f (f x))
end

Sections can be named (section Foo ... end Foo) or anonymous. They nest.

namespace Foo ... end Foo prefixes every name declared inside with Foo.. Use open Foo to bring the short names into scope:

namespace Foo
  def a : Nat := 5
  def f (x : Nat) : Nat := x + a
end Foo

#check Foo.a
  | Foo.a : Nat

open Foo
#check a
  | a : Nat

Sections and namespaces look similar, but they serve different purposes: sections scope variables; namespaces scope names. You can use both. Namespaces can be reopened across files; sections cannot.

The function arrow α → β has a generalization: the return type can depend on the argument. Write (a : α) → β a, where β is a family of types indexed by a:

#check @List.cons
  | @List.cons : {α : Type u_1} → α → List α → List α

Here the output type List α depends on the type argument α. When the return type does not depend on the argument, (a : α) → β is the same as α → β.

Products generalize the same way. (a : α) × β a, also written Σ a : α, β a, is a dependent pair: the second component's type depends on the first component's value. You construct one with ⟨a, b⟩ (or Sigma.mk a b).

This is the feature that puts "dependent" in "dependent type theory." Why that matters is the subject of a separate post; for now, recognize the syntax when you see it.

The compose from the defining functions section required you to pass the types α β γ every time. That's annoying because Lean can usually figure them out from the other arguments. Curly braces mark an argument as implicit: Lean fills it in.

def ident {α : Type} (x : α) : α := x

#check ident 1
  | ident 1 : Nat
#check ident "hello"
  | ident "hello" : String

Four related tools govern how arguments are supplied:

You can also declare implicit parameters with variable by using braces, which is convenient when several definitions in a row share the same one:

variable {α : Type}

def ident (x : α) : α := x

The _ placeholder tells Lean "fill this in at this call site." It's how you supply a single argument while leaving the rest to inference:

#check @ident _ 5
  | ident 5 : Nat

The @ form is how you see the true signature of a function that normally hides its implicits:

#check @ident
  | @ident : {α : Type u_1} → α → α
#check @List.nil
  | @List.nil : {α : Type u_1} → List α

Type ascription is useful when a literal is ambiguous:

#check 2
  | 2 : Nat
#check (2 : Int)
  | 2 : Int

Everything in one place.