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

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

Expected output:

```text id="jnw2eu"
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.

```lean id="codr0z"
def double (n : Nat) : Nat :=
  n + n

#eval double 10
```

Expected output:

```text id="re5a8r"
20
```

This is the simplest way to test small computational definitions.

## Evaluating Functions

Function application works normally under `#eval`.

```lean id="ih0tid"
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:

```text id="z6cktp"
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.

```lean id="w75ozl"
def factorial : Nat -> Nat
| 0 => 1
| n + 1 => (n + 1) * factorial n

#eval factorial 5
```

Expected output:

```text id="t6e9t8"
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.

```lean id="lzywbu"
#eval [1, 2, 3].reverse
#eval some 10
#eval (3, "three")
#eval String.length "Lean"
```

Expected output:

```text id="5h16en"
[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.

```lean id="mcob7l"
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`:

```lean id="rnpxp3"
structure Point where
  x : Nat
  y : Nat
deriving Repr

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

#eval origin
```

Expected output:

```text id="i6t0wg"
{ x := 0, y := 0 }
```

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

## Evaluating `IO`

`#eval` can run `IO` actions.

```lean id="ypnky7"
#eval IO.println "hello from Lean"
```

Expected output:

```text id="z50jsl"
hello from Lean
```

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

A small `IO` example:

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

#eval greet "Lean"
```

Expected output:

```text id="r2zaee"
hello, Lean
```

## Type Ascriptions with `#eval`

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

```lean id="u5ptkl"
#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:

```lean id="b8qfb2"
def emptyList {α : Type} : List α :=
  []

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

Expected output:

```text id="y69fsf"
[]
[]
```

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

## `#eval` and Proofs

Proofs are generally not useful targets for `#eval`.

```lean id="u6qooz"
theorem true_example : True :=
  True.intro
```

You can check the theorem:

```lean id="5j6vyp"
#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.

| Command  | Purpose                     | Example           |
| -------- | --------------------------- | ----------------- |
| `#check` | infer and display a type    | `#check double`   |
| `#eval`  | compute and display a value | `#eval double 10` |

A common workflow is to check first, then evaluate.

```lean id="9cpi5e"
#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.

```lean id="gujtgd"
def normalizeName (s : String) : String :=
  s.trim.toLower

#eval normalizeName "  LEAN  "
```

Expected output:

```text id="fmv5u3"
"lean"
```

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

## Recipe: Build Computation Incrementally

Start with small evaluable definitions.

```lean id="nx3g5d"
def addOne (n : Nat) : Nat :=
  n + 1

#eval addOne 4
```

Then compose them.

```lean id="v0g7ii"
def addTwo (n : Nat) : Nat :=
  addOne (addOne n)

#eval addTwo 4
```

Expected output:

```text id="yv2kis"
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:

```lean id="aqhhya"
#check expression
```

Add a type ascription:

```lean id="drccu2"
#eval (expression : ExpectedType)
```

Check whether the result type has `Repr`:

```lean id="8nn69f"
#check Repr
```

For custom structures, add:

```lean id="g0w0df"
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.