## Stream: general

### Topic: equation has not been used in the compilation

#### Sean Leather (Sep 15 2018 at 08:26):

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 (Sep 15 2018 at 08:26):

you have a match branch that was not used

#### Mario Carneiro (Sep 15 2018 at 08:26):

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


#### Mario Carneiro (Sep 15 2018 at 08:28):

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 (Sep 15 2018 at 08:29):

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


Last updated: May 14 2021 at 03:27 UTC