How to use match expression recursively?

Stream: new members

[Rui Liu]

Is there any way to use match expression in a recursive way? For example in top level equation compiler, you can recurse by use the function name, however, with match expression you don't know the function name.

[Floris van Doorn]

It seems to be possible, but not very convenient to use. The match generates a _match hypothesis that allows for a recursive call, but this hypothesis seems to only be parsed in tactic mode:

def foo (n : ℕ) : ℕ :=
match n + n with
| 0 := 0
| (m+1) := by exact 2 + _match m
end
#eval foo 3 -- 12

If you remove the by exact you get an error unknown identifier '_match'. I guess this rarely comes up, since if you're defining a definition, you usually want to separate out the match statement to a different definition that you can prove properties about.

[Rui Liu]

Thanks! It's indeed a bit inconvenient...