Module 1 · Lesson 6

Debugging & Troubleshooting

How to read Lean's error messages, and how to use #check, #eval and sorry to find what is wrong.

Reading Error Messages

Lean's error messages are detailed and helpful once you learn to read them. They typically include the location, what was expected, and what was found:

lean

Try it

1-- Example error
2def add (x : Nat) (y : Nat) : String := x + y
3-- ERROR: type mismatch
4--   x + y
5-- has type
6--   Nat
7-- but is expected to have type
8--   String
9
10-- The fix: change return type or convert
11def add' (x : Nat) (y : Nat) : Nat := x + y
12def addStr (x : Nat) (y : Nat) : String := toString (x + y)

Key Takeaway

Type mismatch errors tell you exactly what type was expected and what was found. Compare the two: the fix is usually to change one until they agree.

Using #check

The #check command shows the type of any expression. Use it to understand what you're working with:

lean

Try it

1-- Check types of values
2#check 42           -- Nat
3#check "hello"      -- String
4#check true         -- Bool
5
6-- Check types of functions
7#check Nat.add      -- Nat.add : Nat → Nat → Nat
8#check List.map     -- List.map {α : Type u_1} {β : Type u_2} (f : α → β) (l : List α) : List β
9
10-- Check complex expressions
11#check (fun (x : Nat) => x + 1)   -- Nat → Nat
12#check [1, 2, 3].map              -- (Nat → ?m) → List ?m  (β not yet known)
13
14-- Check with explicit types
15#check (42 : Int)         -- Int
16#check ([] : List String) -- List String

Using #eval

#eval runs code and shows the result. Great for testing expressions interactively:

lean

Try it

1-- Test computations
2#eval 2 + 3           -- 5
3#eval [1, 2, 3].length -- 3
4#eval "hello".toUpper -- "HELLO"
5
6-- Test functions
7def double (n : Nat) := n * 2
8#eval double 5        -- 10
9
10-- Test complex expressions
11#eval [1, 2, 3].map (· * 2) |> List.sum  -- 12
12
13-- #eval CAN run IO — the output goes to the infoview
14#eval IO.println "hi"        -- prints: hi
15
16-- ...including a whole do block
17#eval do
18  IO.println "step 1"
19  IO.println "step 2"
20  return 42

ℹ

What #eval cannot do is print a value whose type has no Repr or ToStringinstance — functions, most of all. #eval (· + 1)fails with could not synthesize a Repr instance, not because evaluation failed but because Lean does not know how to show you the answer. Apply the function to something, or use #check.

Using #print

#print shows the full definition of a name. Useful for understanding library functions:

lean

Try it

1-- See how things are defined
2#print Nat.add
3#print List.map
4#print Bool
5
6-- Great for understanding type class instances.
7-- Trick: ask for the instance first, then print the name it reports.
8#check (inferInstance : BEq Nat)
9#print instBEqOfDecidableEq   -- how Nat's BEq is actually built
10
11-- Related commands
12#print axioms List.map        -- what a definition/proof depends on
13#print equations Nat.add      -- the defining equations, as simp can use them

Making Lean Show More

Half of debugging is getting Lean to stop hiding things. Pretty-printing options turn implicit arguments, coercions, and instances back on:

lean

Try it

1-- Show every implicit argument and instance
2set_option pp.explicit true in
3#check @List.map
4
5-- Show the type of every numeral (great for Nat-vs-Int confusion)
6set_option pp.numericTypes true in
7#check (42 : Int)          -- (42 : Int) : Int
8
9-- Show coercions that are normally invisible
10set_option pp.coercions true in
11example (n : Nat) : (n : Int) = n := rfl
12
13-- The blunt instrument: show absolutely everything
14set_option pp.all true in
15#check 1 + 1
16
17-- Scope it to one command with "in", or to the rest of the file
18-- by writing set_option ... on its own line.

💡

When an error says two things are different but they look identical on screen, set_option pp.explicit true almost always reveals the difference — usually a different instance or a hidden coercion.

dbg_trace and assert!

For pure functions you cannot sprinkle IO.printlncalls. dbg_trace is the escape hatch: it prints when the expression is evaluated, and is invisible to the type system.

lean

Try it

1def f (n : Nat) : Nat :=
2  dbg_trace s!"f called with {n}"
3  n * 2
4
5#eval f 3
6-- f called with 3
7-- 6
8
9-- assert! checks a condition at runtime and panics if it fails
10#eval assert! 1 + 1 == 2; "ok"   -- "ok"
11
12-- #check_failure asserts that something does NOT typecheck.
13-- Useful in teaching material and regression tests.
14#check_failure (42 : String)

⚠

dbg_trace fires during evaluation, not during elaboration, and it is skipped entirely inside proofs. It is a debugging aid for programs, not for tactics — for those, use trace_state below.

Common Errors and Fixes

Type Mismatch

lean

Try it

1-- Problem: wrong type
2-- def f : String := 42
3
4-- Fix 1: Change the annotation
5def f : Nat := 42
6
7-- Fix 2: Convert the value
8def g : String := toString 42

Unknown Identifier

lean

Try it

1-- Problem: name not in scope
2-- #eval unknownFunction
3
4-- Common causes:
5-- 1. Typo in the name
6-- 2. Missing import (imports MUST be at the very top of the file)
7-- 3. Right function, wrong namespace
8
9-- Fix 3a: use the fully qualified name
10#eval List.head? [1, 2]           -- some 1
11
12-- Fix 3b: open the namespace, for one command or for the rest of the file
13open List in
14#eval head? [1, 2]                -- some 1
15
16-- Fix 3c: dot notation resolves the namespace from the type — usually best
17#eval [1, 2].head?                -- some 1

⚠

import lines must come before everything else in a file — before the first def, before any comment-free code. If you add import Mathlibhalfway down, Lean reports a parse error on the import, not on the name you were trying to fix.

Function Expected

lean

Try it

1def add (x y : Nat) : Nat := x + y
2
3-- Problem: applying a non-function
4-- #eval 42 5          -- Error: function expected, 42 is a Nat
5
6-- The usual real cause is missing parentheses. Application binds tighter
7-- than any operator, so this is read as ((add 1 2) 3) — three arguments
8-- handed to a two-argument function.
9-- #eval add 1 2 3
10
11-- Fix: parenthesise what you meant
12#eval (add 1 2) + 3    -- 6
13#eval add 1 (2 + 3)    -- 6
14
15-- Same trap with negative numbers — the minus is read as subtraction:
16-- #eval add 1 -2
17-- failed to synthesize HSub (Nat → Nat) Nat ?m   ← i.e. (add 1) - 2
18#eval add 1 (-2 : Int).toNat   -- 1

Failed to Synthesize Instance

lean

Try it

1-- Problem: type class instance not found
2def eq [BEq α] (x y : α) := x == y
3-- #eval eq (fun (_ : Nat) => 1) (fun _ => 1)
4-- Error: failed to synthesize BEq (Nat → Nat)  — functions have no decidable equality
5
6-- Fix: use a type that has the instance
7#eval eq (5 : Nat) 5   -- true
8
9-- Read the message as a question: "does this type support this operation?"
10--   failed to synthesize  Repr X       → #eval cannot display an X
11--   failed to synthesize  OfNat X 42   → 42 is not a valid X literal
12--   failed to synthesize  Decidable p  → p cannot be turned into a Bool
13--   failed to synthesize  Inhabited X  → X might be empty, so no default value
14
15-- Diagnose by asking for the instance directly:
16#check (inferInstance : BEq Nat)         -- ok
17-- #check (inferInstance : BEq (Nat → Nat))  -- fails, and says exactly why

Debugging Proofs: trace and trace_state

Inside a proof, trace prints a message and trace_state prints the current goal and hypotheses. Both are no-ops for the proof itself — they only talk to you.

lean

Try it

1example (n : Nat) : n + 0 = n := by
2  trace "about to simp"
3  trace_state
4  -- n : Nat
5  -- ⊢ n + 0 = n
6  simp

⚠

Do not put a tactic after the one that closes the goal — simp followed by trace "done"fails with no goals. To see the state after a step, put trace_state before the next step, or just move your cursor there and read the infoview.

For seeing what a tactic did internally, the trace. options are more informative than any print:

lean

Try it

1-- Which simp lemmas actually fired?
2set_option trace.Meta.Tactic.simp true in
3example (n : Nat) : n + 0 = n := by simp
4
5-- Why did instance search fail?
6set_option trace.Meta.synthInstance true in
7#check (inferInstance : BEq Nat)
8
9-- simp? / says: get simp to print the exact "simp only [...]" it used,
10-- so you can paste it back and make the proof fast and stable.
11example (n : Nat) : n + 0 = n := by simp?

The sorry Tactic

sorry lets you skip parts of a proof temporarily. Useful for exploring structure:

lean

Try it

1-- Sketch a proof structure, fill in later
2theorem complex_proof (n : Nat) : n + 0 = n ∧ 0 + n = n := by
3  constructor
4  · sorry  -- First part
5  · sorry  -- Second part
6
7-- Warning: sorry makes proofs invalid!
8-- Lean shows a warning when sorry is used

⚠

sorry introduces the axiom sorryAx, from which anything follows. The danger is not the sorry you can see — it is the one three files away that some theorem you are using quietly depends on. Lean warns at the definition site only.

lean

Try it

1theorem shaky : 1 = 2 := by sorry   -- warning: declaration uses 'sorry'
2
3-- No warning here! The dependency is invisible at the use site.
4theorem builtOnSand : 2 = 1 := shaky.symm
5
6-- This is how you catch it:
7#print axioms builtOnSand
8-- 'builtOnSand' depends on axioms: [sorryAx]
9
10-- A clean result looks like this:
11theorem solid : 1 + 1 = 2 := rfl
12#print axioms solid
13-- 'solid' does not depend on any axioms

💡

Make #print axioms yourMainTheorem the last line of any file you care about. Seeing only propext, Classical.choice, and Quot.sound is normal and fine — those are the three standard axioms of Lean's logic. Seeing sorryAx is not.

Best Practices

Check types often. Many errors come from a value having a different type than you assumed.
Test small pieces. Run a function with #eval before you build on it.
Read the whole error message. The expected and the actual type are usually both in it.
Sketch with sorry. Then replace one sorry at a time.
Check imports. An "unknown identifier" error often means a missing import.

Exercise: Debug This

Fix the type error in this code:

lean

Try it

1-- This has an error
2-- def greet (name : String) : Nat := "Hello, " ++ name
3
4-- Fixed version
5def greet (name : String) : String := "Hello, " ++ name

Syntax & Notation Next: Structures