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 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) live in a separate post.

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 and String are 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, and 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 do different jobs.

A section scopes variable declarations. Variables declared inside a section are forgotten at end. The definitions written inside still exist with their auto-bound parameters baked in, but the section itself leaves nothing behind. Sections affect elaboration, not the names that survive.

A namespace scopes names instead. Every def inside namespace Foo becomes Foo.<name>, and that prefix is permanent. open Foo brings the short names back into scope at the use site, but the underlying name is still Foo.<name>.

The two are orthogonal. You can nest a section inside a namespace or the other way around; a common pattern is a namespace Foo containing several sections, each with its own variable block.

Namespaces can also be reopened. Writing namespace Foo again, in the same file or another, adds more declarations to Foo. Sections cannot be reopened; once end runs, the section is gone.

The function arrow α → β has a generalization. In an ordinary arrow, the return type β is fixed. Every input of type α produces an output of the same type β. The generalization lets β vary with the argument, so different inputs can produce outputs of different types.

Write this as (a : α) → β a. The argument now has a name, a, so the return type can refer to it. β is a family of types indexed by a (a function from values of α to types), and β a picks out the specific return type for the specific input:

#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).

For instance, define a type family Pick : Bool → Type that maps true to Nat and false to String. The same Sigma type then holds pairs whose second components have different types:

def Pick : Bool → Type
  | true  => Nat
  | false => String

#check (⟨true, 5⟩ : Σ b : Bool, Pick b)
  | ⟨true, 5⟩ : (b : Bool) × Pick b
#check (⟨false, "hi"⟩ : Σ b : Bool, Pick b)
  | ⟨false, "hi"⟩ : (b : Bool) × Pick 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 forced every caller to spell out α β γ, even though Lean could read those off the other arguments. Wrap a parameter in curly braces and Lean fills it in instead:

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

def double (n : Nat) : Nat := n + n
def isEven (n : Nat) : Bool := n % 2 == 0

#check compose isEven double
  | compose isEven double : Nat → Bool
#eval compose isEven double 4
  | true

No types appear at the call site. Lean reads α, β, γ off the signatures of isEven and double. The same braces work on any single parameter Lean can infer:

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

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

The implicit/explicit choice lives in two places: how you declare a parameter and how you supply it at a call site. Two declaration forms, two call-site overrides:

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 α

A related annotation, type ascription (e : T), tells Lean to treat e as having type T. Useful when a literal is ambiguous:

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