Zulip Chat Archive

Stream: general

Topic: equation has not been used in the compilation


view this post on Zulip 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)

view this post on Zulip Mario Carneiro (Sep 15 2018 at 08:26):

you have a match branch that was not used

view this post on Zulip Mario Carneiro (Sep 15 2018 at 08:26):

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

view this post on Zulip 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

view this post on Zulip 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