Equation compiler error

Stream: general

[Seul Baek]

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?

[Kenny Lau]

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

[Kenny Lau]

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

[Kevin Buzzard]

rofl

[Kenny Lau]

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

[Chris Hughes]

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

[Dan Velleman]

I am trying to use a match statement in the definition of a tactic. If I have more than 5 cases in the match, I get the error message "equation compiler failed, maximum number of steps (2048) exceeded." Is there a limit of 5 cases in a match?

[Yakov Pechersky]

(deleted)

[Eric Wieser]

It sounds like each of your cases is rather complex

[Dan Velleman]

They're just pattern matching on an expression.

[Dan Velleman]

I have a workaround: a smaller number of cases, and each case calls a function with a few cases. But I'm surprised that I had to resort to that.

[Eric Wieser]

Without a #mwe or at least a link to a github repo with failing code, I doubt anyone can diagnose further.