Zulip Chat Archive

Stream: general

Topic: Equation compiler error


view this post on Zulip Seul Baek (Mar 02 2019 at 22:39):

def foo : bool → nat → unit
| tt 0     := ()
| tt m     := ()
| ff 0     := ()
| ff (m+1) := foo ff m

For some reason Lean thinks the second case is unnecessary and gives an equation compiler error. If I remove the case, however, it correctly reports that I'm missing the case foo tt (nat.succ _). I wonder what's going on here?

view this post on Zulip Kenny Lau (Mar 02 2019 at 22:41):

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

view this post on Zulip Kenny Lau (Mar 02 2019 at 22:42):

(lawyer mode) they didn't say delete equation 2 :P

view this post on Zulip Kevin Buzzard (Mar 02 2019 at 22:42):

rofl

view this post on Zulip Kenny Lau (Mar 02 2019 at 22:42):

(lawyer mode) I deleted equation 1 and it worked, so the error message isn't lying

view this post on Zulip Chris Hughes (Mar 02 2019 at 22:42):

I think it was used

def foo : bool  nat  bool
| tt 0     := ff
| tt m     := tt
| ff 0     := ff
| ff (m+1) := foo ff m

#eval foo tt 1

Last updated: May 15 2021 at 00:39 UTC