1.5 Definitions with `def`

A definition introduces a named term together with its type. In Lean, definitions serve two roles at once: they define computations and they provide reusable building blocks for proofs. The kernel treats a definition as a constant whose value is an expression, and subsequent elaboration may unfold that value when needed.

Problem

You want to introduce reusable functions and constants, control how they are reduced during proofs, and understand how definitions interact with the type system.

Solution

Use def to bind a name to an expression with a specified type.

def one : Nat :=
  1

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

Check and evaluate:

#check one
#check add
#eval add 3 4

Expected result:

Structure of a Definition

The general form is:

def name (parameters) : Type :=
  expression

Lean checks that expression has the declared type.

Parameters may be explicit:

def square (x : Nat) : Nat :=
  x * x

or implicit:

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

Implicit parameters are inferred by the elaborator.

Definitional Equality

Definitions are transparent by default. Lean may replace a defined name with its value during type checking and rewriting.

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

#check double 3
#eval double 3

Lean treats double 3 and 3 + 3 as definitionally equal. This equality requires no proof and is resolved by computation.

This property is central. Many proofs succeed because Lean can reduce definitions automatically.

Parameter Handling

Multiple parameters can be grouped:

def addThree (x y z : Nat) : Nat :=
  x + y + z

This is equivalent to a curried function:

Nat -> Nat -> Nat -> Nat

Partial application works:

#check addThree 1 2

This expression has type Nat -> Nat.

Implicit Arguments

Implicit arguments are enclosed in braces:

def const {α β : Type} (x : α) (y : β) : α :=
  x

Lean infers α and β from usage:

#check const 5 true

Result:

const 5 true : Nat

You can force explicit arguments using @:

#check @const Nat Bool 5 true

Let-Bound Definitions Inside Terms

Local definitions use let:

#eval
  let x := 10
  let y := 20
  x + y

These are not global declarations. They exist only within the expression.

Recursive Definitions

Recursive functions must satisfy termination checking.

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

Evaluate:

#eval factorial 5

Expected result:

Lean verifies that recursion decreases structurally.

Pattern Matching in Definitions

Definitions often use pattern matching:

def pred : Nat -> Nat
| 0     => 0
| n + 1 => n

This defines the predecessor function.

Pattern matching is compiled into eliminators for inductive types.

Noncomputable Definitions

Some definitions depend on classical reasoning and cannot be evaluated.

noncomputable def choice_example (α : Type) [Inhabited α] : α :=
  default

The keyword noncomputable marks such definitions explicitly.

Opaque vs Transparent

By default, definitions are transparent. Lean unfolds them during reduction.

In some contexts, you may want to prevent unfolding. This is handled by attributes such as:

@[irreducible]
def hidden (n : Nat) : Nat :=
  n + 1

This affects how aggressively Lean simplifies expressions.

Control over unfolding becomes important in large proofs and automation tuning.

Definitions vs Theorems

A definition:

def two : Nat := 2

A theorem:

theorem two_eq : two = 2 := rfl

Both bind names to expressions. The difference lies in the type:

definitions produce data or functions
theorems produce proofs of propositions

At the kernel level, both are constants with values.

Namespaces and Definitions

Definitions live inside namespaces:

namespace Myproj

def inc (n : Nat) : Nat :=
  n + 1

end Myproj

Use:

#eval Myproj.inc 5

Namespaces prevent name collisions and organize code.

Minimal Working Example

def triple (n : Nat) : Nat :=
  n + n + n

#eval triple 7

Expected result:

Common Pitfalls

If Lean cannot infer a type, add explicit annotations.

If recursion is rejected, ensure the argument decreases structurally.

If a definition does not simplify as expected, check transparency or unfolding behavior.

If implicit arguments are not inferred, use @ to expose them.

If names clash, use namespaces or qualified names.

Takeaway

def introduces named expressions that Lean can compute and unfold automatically. Transparent definitions support definitional equality, which reduces proof burden. Careful control of parameters, recursion, and unfolding leads to predictable behavior in both computation and proof development.