1.12 Evaluation with `#eval`

Lean can execute many expressions during development. The command #eval asks Lean to compute an expression and print the result. This is useful for testing definitions, inspecting small examples, and confirming that executable code behaves as intended.

Problem

You want to run Lean expressions directly inside a source file and see their computed results.

Solution

Use #eval followed by an expression.

#eval 2 + 3
#eval "Lean" ++ " Cookbook"
#eval List.map (fun n : Nat => n + 1) [1, 2, 3]

Expected output:

5
"Lean Cookbook"
[2, 3, 4]

#eval does not create a declaration. It is a command that asks Lean to evaluate an expression and display the result in the editor or terminal output.

Evaluating Definitions

A definition can be evaluated after it is declared.

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

#eval double 10

Expected output:

20

This is the simplest way to test small computational definitions.

Evaluating Functions

Function application works normally under #eval.

def applyTwice (f : Nat -> Nat) (x : Nat) : Nat :=
  f (f x)

#eval applyTwice (fun n => n + 1) 10
#eval applyTwice (fun n => n * 2) 10

Expected output:

12
40

Lean evaluates the expression after elaborating it. Type inference, implicit arguments, and notation are resolved before computation begins.

Evaluating Recursive Definitions

Recursive definitions can also be evaluated, provided Lean accepts their termination.

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

#eval factorial 5

Expected output:

120

The definition is executable because each recursive call is made on a structurally smaller natural number.

Evaluating Data Structures

#eval is especially useful with lists, options, products, and strings.

#eval [1, 2, 3].reverse
#eval some 10
#eval (3, "three")
#eval String.length "Lean"

Expected output:

[3, 2, 1]
some 10
(3, "three")
4

The result must have a printable representation. In practice, this usually means Lean can synthesize a Repr instance for the result type.

When Printing Fails

Some values can be computed but cannot be printed.

structure Point where
  x : Nat
  y : Nat

def origin : Point :=
  { x := 0, y := 0 }

-- #eval origin

This may fail because Lean does not know how to display Point.

Derive Repr:

structure Point where
  x : Nat
  y : Nat
deriving Repr

def origin : Point :=
  { x := 0, y := 0 }

#eval origin

Expected output:

{ x := 0, y := 0 }

The deriving Repr clause asks Lean to generate a printable representation.

Evaluating IO

#eval can run IO actions.

#eval IO.println "hello from Lean"

Expected output:

hello from Lean

For ordinary expressions, #eval prints the computed value. For IO actions, it runs the action.

A small IO example:

def greet (name : String) : IO Unit := do
  IO.println s!"hello, {name}"

#eval greet "Lean"

Expected output:

hello, Lean

Type Ascriptions with #eval

When literals or overloaded operations are ambiguous, add a type ascription.

#eval (0 : Nat)
#eval (0 : Int)
#eval ((2 : Nat) + 3)

A type ascription tells Lean which instance and representation to use.

This is often needed when evaluating polymorphic expressions:

def emptyList {α : Type} : List α :=
  []

#eval (emptyList : List Nat)
#eval (emptyList : List String)

Expected output:

[]
[]

Without the type ascription, Lean may not know which element type to choose.

#eval and Proofs

Proofs are generally not useful targets for #eval.

theorem true_example : True :=
  True.intro

You can check the theorem:

#check true_example

but evaluating proof terms usually gives little useful information. Proofs live in Prop, and Lean treats them as computationally irrelevant.

Use #eval for executable data and #check for types and proof statements.

#eval vs #check

The commands serve different purposes.

A common workflow is to check first, then evaluate.

#check List.map
#eval List.map (fun n : Nat => n + 1) [1, 2, 3]

This reduces guessing. #check tells you the expected shape of the expression. #eval confirms the computation.

#eval Inside Projects

#eval commands are checked when the file is elaborated. They are useful during development, but they can slow down large files if the computation is expensive.

For small examples, keep them near the definitions they test.

def normalizeName (s : String) : String :=
  s.trim.toLower

#eval normalizeName "  LEAN  "

Expected output:

"lean"

For larger tests, prefer separate test files or executable entry points.

Recipe: Build Computation Incrementally

Start with small evaluable definitions.

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

#eval addOne 4

Then compose them.

def addTwo (n : Nat) : Nat :=
  addOne (addOne n)

#eval addTwo 4

Expected output:

6

This pattern helps isolate failures. If addTwo behaves incorrectly, first evaluate addOne.

Recipe: Debug a Failed Evaluation

When #eval fails, separate the possible causes.

Check the type:

#check expression

Add a type ascription:

#eval (expression : ExpectedType)

Check whether the result type has Repr:

#check Repr

For custom structures, add:

deriving Repr

For recursive functions, confirm that the definition compiled before evaluating it.

Common Pitfalls

If Lean cannot print a result, derive or provide a Repr instance.

If Lean cannot infer a type, add a type ascription.

If evaluation does not terminate, the definition may be partial, recursive through unsafe mechanisms, or computationally expensive.

If an expression contains noncomputable components, #eval cannot execute it as ordinary code.

If #eval slows the file, move large computations to a separate executable or test file.

Takeaway

#eval is the quickest way to execute Lean code during development. It works best for concrete, computable expressions with printable result types. Use it with #check: first inspect the type, then evaluate the value. This keeps small definitions honest and makes executable examples part of the source file.