equation has not been used in the compilation

Stream: general

[Sean Leather]

This is the first time I've seen the error below. What does it mean? What might be causing it?

error: equation compiler error, equation #2 has not been used in the compilation (possible solution: delete equation)

[Mario Carneiro]

you have a match branch that was not used

[Mario Carneiro]

def f : ℕ → ℕ
| n := n + 1
| 0 := 0

[Mario Carneiro]

It is often caused by a constant in your pattern actually being interpreted as a variable and thus being more generic than it is supposed to be

[Mario Carneiro]

def f : ℕ → ℕ
| zero := 1 -- zero is a variable since it should be nat.zero
| (n+1) := n -- not used