using induction hypothesis in match

Stream: general

[Chris Hughes]

Why does the second one work but not the first?

def id1 (x : ℕ) : ℕ :=
match x with
| 0 := 0
| (n+1) := _match n + 1 --fails
end

def id2 (x : ℕ) : ℕ :=
match x with
| 0 := 0
| (n+1) := by exact _match n + 1 --works
end

[Mohammad Pedramfar]

(deleted)

[Sebastian Ullrich]

Because the first one is intended to not work and the second one is not intended to work

[Bryan Gin-ge Chen]

I noticed this too, back here; I guess we're "supposed to" put x to the right of the colon like Mario did in that thread.

[Chris Hughes]

Sometimes x isn't an argument to the function however, it's something defined later.

[Mario Carneiro]

the "official" solution is to just have an auxiliary function, or use induction to construct the function. In lean 4, if my suggestion to sebastian worked, we will have an actual term mode notation for this using let