Defining Functions and Constants in Lean 4

Functions and constants are the primary building blocks of any Lean 4 program or proof. Lean 4 uses a unified declaration syntax where def, theorem, lemma, and abbrev all introduce names into the environment — the difference lies in their intended use and how the elaborator and optimizer treat them. This page covers every form of definition you will encounter, from simple constants to well-founded recursive functions.

Basic Declarations

`def` — Definitions

def introduces a computable definition:

-- Constant
def pi : Float := 3.141592653589793

-- Function (explicit argument)
def square (n : Nat) : Nat := n * n

-- With return type inferred
def greet name := "Hello, " ++ name ++ "!"

#eval square 7    -- 49
#eval greet "Lean"  -- "Hello, Lean!"

`theorem` and `lemma`

theorem and lemma are definitionally identical to def but signal to readers (and the compiler) that the term is a proof. The elaborator marks them as opaque by default, so they do not reduce under normal evaluation — this is intentional for proof performance.

theorem add_comm' (a b : Nat) : a + b = b + a := by
  omega

lemma zero_add' (n : Nat) : 0 + n = n := by
  simp

`abbrev` — Abbreviations

abbrev declares a definition that is always unfolded by the elaborator (at every transparency level). Use it for type aliases or short wrappers where you want the definition to be transparent everywhere:

abbrev Point := Nat × Nat

-- Because Point is an abbrev, the elaborator sees through it
def origin : Point := (0, 0)

`noncomputable`

Mark a definition noncomputable when it uses classical axioms (Classical.choice) or is otherwise not executable. The compiler will refuse to generate code for it, but it can still be used in proofs:

-- Classical.choice requires a nonemptiness axiom and cannot be executed
noncomputable def someValue : Nat := Classical.choice ⟨0⟩

-- You can still prove things about it in proofs
example : True := trivial

Lambda Expressions

-- Basic lambda
def double : Nat → Nat := fun n => n * 2

-- Multiple arguments
def add : Nat → Nat → Nat := fun a b => a + b

-- Pattern-matching lambda (fun with |)
def describeOpt : Option Nat → String := fun
  | some n => s!"Got {n}"
  | none   => "Nothing"

-- Shorthand anonymous function (placeholder syntax)
#eval [1, 2, 3].map (· * 10)   -- [10, 20, 30]
#eval [1, 2, 3, 4].filter (· % 2 == 0)  -- [2, 4]

Argument Kinds

Explicit Arguments `(a : α)`

The caller must supply the argument explicitly:

def repeatStr (s : String) (n : Nat) : String :=
  String.join (List.replicate n s)

#eval repeatStr "ha" 3   -- "hahaha"

Implicit Arguments `{a : α}`

Curly-brace arguments are inferred by the unifier. The caller does not (normally) provide them:

def id' {α : Type*} (a : α) : α := a

#eval id' 42        -- 42  (α is inferred as Nat)
#eval id' "hello"   -- "hello"  (α is inferred as String)

-- Force explicit with @
#eval @id' Nat 42   -- 42

Instance Arguments `[inst : Class α]`

Square-bracket arguments are filled by typeclass synthesis:

def showTwice [ToString α] (a : α) : String :=
  toString a ++ ", " ++ toString a

#eval showTwice 42        -- "42, 42"
#eval showTwice "hello"   -- "hello, hello"

You can name the instance or leave it anonymous:

def sum' [Add α] [Zero α] (xs : List α) : α :=
  xs.foldl (· + ·) 0

Auto-Bound Implicit Variables

Any lowercase variable used in a type signature but not declared is automatically bound as an implicit argument. This reduces verbosity:

-- α is auto-bound as {α : Type*}
def myLength (xs : List α) : Nat :=
  match xs with
  | []      => 0
  | _ :: t => 1 + myLength t

-- Equivalent to:
-- def myLength {α : Type*} (xs : List α) : Nat := ...

Auto-bound implicit works for lowercase names only. To declare universe variables that should be auto-bound, use universe u at the top of a section.

Optional and Named Arguments

-- Optional argument with default value
def greetFormal (name : String) (greeting : String := "Hello") : String :=
  s!"{greeting}, {name}!"

#eval greetFormal "Alice"              -- "Hello, Alice!"
#eval greetFormal "Alice" "Greetings"  -- "Greetings, Alice!"

-- Named argument (pass out of order)
#eval greetFormal (greeting := "Hi") "Bob"  -- "Hi, Bob!"

Recursive Functions

Structural Recursion

The most common form: recurse on a structurally smaller subterm. Lean’s termination checker accepts this automatically:

def factorial : Nat → Nat
  | 0     => 1
  | n + 1 => (n + 1) * factorial n

def listSum : List Nat → Nat
  | []      => 0
  | x :: xs => x + listSum xs

#eval factorial 10    -- 3628800
#eval listSum [1, 2, 3, 4, 5]  -- 15

Fibonacci with Accumulator

def fib (n : Nat) : Nat :=
  go n 0 1
where
  go : Nat → Nat → Nat → Nat
    | 0,     a, _ => a
    | n + 1, a, b => go n b (a + b)

#eval fib 30    -- 832040

Well-Founded Recursion

When structural recursion does not apply, Lean can use well-founded recursion. Provide a termination_by clause with a decreasing measure:

def collatz (n : Nat) : Nat :=
  if n ≤ 1 then 0
  else if n % 2 == 0 then 1 + collatz (n / 2)
  else 1 + collatz (3 * n + 1)
termination_by n   -- the argument n must decrease; Lean uses a well-founded order

#eval collatz 27    -- 111

For mutual recursion, use mutual ... end:

mutual
  def isEven : Nat → Bool
    | 0     => true
    | n + 1 => isOdd n

  def isOdd : Nat → Bool
    | 0     => false
    | n + 1 => isEven n
end

#eval isEven 42   -- true
#eval isOdd  7    -- true

`partial def` — Potentially Non-Terminating Functions

When termination cannot be proved (or when you intentionally want a potentially non-terminating function), use partial def. The function is accepted without a termination check, but it cannot be used in proofs:

partial def infiniteLoop : IO Unit := do
  IO.println "tick"
  infiniteLoop

-- Also useful for I/O servers, interpreters, etc.
partial def repl : IO Unit := do
  let line ← (← IO.getStdin).getLine
  if line.trim == "quit" then return
  IO.println s!"Echo: {line}"
  repl

partial functions can loop forever. They are excluded from the kernel, so they cannot appear in proofs or be evaluated during elaboration.

Dot Notation and Projection

Lean 4 supports dot notation for namespace dispatch:

-- Equivalent calls
#eval List.length [1, 2, 3]
#eval [1, 2, 3].length

-- Dot notation finds definitions in the namespace matching the head type
def List.second? (xs : List α) : Option α := xs.tail.head?
#eval [10, 20, 30].second?   -- some 20

Key Attributes on Definitions

Attributes control elaboration, optimization, and the simp set:

`@[simp]`

Adds the definition or theorem to the global simp set, so simp will use it automatically:

@[simp]
theorem list_length_nil : ([] : List α).length = 0 := rfl

@[simp]
theorem list_length_cons (x : α) (xs : List α) :
    (x :: xs).length = xs.length + 1 := rfl

`@[inline]`

Instructs the compiler to inline the function at every call site. Use for small, hot-path functions:

@[inline]
def increment (n : Nat) : Nat := n + 1

`@[reducible]`

Makes the definition visible at reducible transparency. Useful for type aliases that should be seen through by typeclass search:

@[reducible]
def MyList α := List α

-- Typeclass instances for List α now apply to MyList α too

`@[extern]`

Links the definition to a C function implementation. The Lean declaration provides the type signature; the runtime uses the C function:

@[extern "lean_nat_add"]
protected def Nat.add : Nat → Nat → Nat
  | a, .zero   => a
  | a, .succ b => .succ (Nat.add a b)

`#check` and `#eval` for Functions

#check List.map      -- List.map : (α → β) → List α → List β
#check @List.foldl   -- @List.foldl : {α : Type u_1} → {β : Type u_2} → (α → β → α) → α → List β → α
#eval (fun x => x * x) 9   -- 81

Introduction

Language Basics

Theorem Proving

Functional Programming

Defining Functions and Constants in Lean 4

Basic Declarations

`def` — Definitions

`theorem` and `lemma`

`abbrev` — Abbreviations

`noncomputable`

Lambda Expressions

Argument Kinds

Explicit Arguments `(a : α)`

Implicit Arguments `{a : α}`

Instance Arguments `[inst : Class α]`

Auto-Bound Implicit Variables

Optional and Named Arguments

Recursive Functions

Structural Recursion

Fibonacci with Accumulator

Well-Founded Recursion

`partial def` — Potentially Non-Terminating Functions

Dot Notation and Projection

Key Attributes on Definitions

`@[simp]`

`@[inline]`

`@[reducible]`

`@[extern]`

`#check` and `#eval` for Functions

Build docs developers (and LLMs) love

Introduction

Language Basics

Theorem Proving

Functional Programming

Documentation Index

​Basic Declarations

​def — Definitions

​theorem and lemma

​abbrev — Abbreviations

​noncomputable

​Lambda Expressions

​Argument Kinds

​Explicit Arguments (a : α)

​Implicit Arguments {a : α}

​Instance Arguments [inst : Class α]

​Auto-Bound Implicit Variables

​Optional and Named Arguments

​Recursive Functions

​Structural Recursion

​Fibonacci with Accumulator

​Well-Founded Recursion

​partial def — Potentially Non-Terminating Functions

​Dot Notation and Projection

​Key Attributes on Definitions

​@[simp]

​@[inline]

​@[reducible]

​@[extern]

​#check and #eval for Functions

Build docs developers (and LLMs) love

Basic Declarations

`def` — Definitions

`theorem` and `lemma`

`abbrev` — Abbreviations

`noncomputable`

Lambda Expressions

Argument Kinds

Explicit Arguments `(a : α)`

Implicit Arguments `{a : α}`

Instance Arguments `[inst : Class α]`

Auto-Bound Implicit Variables

Optional and Named Arguments

Recursive Functions

Structural Recursion

Fibonacci with Accumulator

Well-Founded Recursion

`partial def` — Potentially Non-Terminating Functions

Dot Notation and Projection

Key Attributes on Definitions

`@[simp]`

`@[inline]`

`@[reducible]`

`@[extern]`

`#check` and `#eval` for Functions