recursion with multiple inputs

Stream: new members

[Britt Anderson]

Why can't lean figure out that this will end? Or why can't I figure out what Lean is doing?

def test : Nat -> Nat -> Nat
| 0, _ => 1
| x, 0 => 1
| x, y => test (x - 1) (y - 1)

#eval test 1 2

[Damiano Testa]

Does using x + 1, y + 1 instead, work?

[Joachim Breitner]

The information that x isn't 0 is not available in the last branch. Try using pattern matching on the left (x + 1, y +1 =>)

[Britt Anderson]

Damiano Testa said:

Does using x + 1, y + 1 instead, work?

Yes.

[Britt Anderson]

Joachim Breitner said:

The information that x isn't 0 is not available in the last branch. Try using pattern matching on the left (x + 1, y +1 =>)

So, I cannot (should not) infer that Lean will check the patterns in order?

[Joachim Breitner]

It does, but it doesn't add that information to the context, as in general that may blow up in size. You could use if h : x = 0… here