Module 1 · Lesson 6

Debugging & Troubleshooting

Learn essential techniques for understanding and fixing errors in Lean. From reading error messages to using #check and #eval, these tools will help you debug code effectively.

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

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. Read both carefully—the fix is usually making them match.

Using #check

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

lean

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

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

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

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

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

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

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

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

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

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

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

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

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.soundis normal and fine — those are the three standard axioms of Lean's logic. Seeing sorryAx is not.

Best Practices

Use #check liberally — Type confusion is the #1 source of errors
Test small pieces — Use #eval to test functions before using them
Read error messages fully — They often contain the solution
Use sorry to sketch — Then fill in one piece at a time
Check imports— Many "unknown identifier" errors are missing imports

Exercise: Debug This

Fix the type error in this code:

lean

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