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 #check command 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 → Nat → Nat
8#check List.map     -- {α β : Type} → (α → β) → List α → List β
9
10-- Check complex expressions
11#check (fun x => x + 1)   -- Nat → Nat
12#check [1, 2, 3].map      -- (Nat → β) → List β
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-- Can't eval functions that need IO
14-- #eval IO.println "hi"  -- Error
15-- Use #eval do instead:
16-- (Run in main or with IO.println disabled)

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#print instBEqNat  -- How Nat equality works

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
7-- 3. Wrong namespace
8
9-- Fix: Check spelling, add import, or use full name
10import Mathlib.Tactic  -- Add import
11open List in #eval head? [1, 2]  -- Open namespace

Function Expected

lean

1-- Problem: applying non-function
2-- #eval 42 5  -- Error: 42 is not a function
3
4-- This often happens with missing parentheses
5-- #eval add 1 2 3  -- If add takes 2 args, this is wrong
6
7-- Fix: Check function arity and add parens
8#eval (add 1 2) + 3

Failed to Synthesize Instance

lean

1-- Problem: type class instance not found
2-- def eq [BEq α] (x y : α) := x == y
3-- #eval eq (fun _ => 1) (fun _ => 1)  -- No BEq for functions!
4
5-- Fix: Use only types with the required instance
6#eval (5 : Nat) == 5  -- Nat has BEq ✓

Debugging Tactics: trace

In proofs, trace prints debug information:

lean

1example : 2 + 2 = 4 := by
2  trace "Before simp"
3  simp
4  trace "After simp"  -- Won't run, goal is closed

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

⚠

Never submit code with sorry in production. It axiomatically assumes anything is true, which can lead to inconsistencies.

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