## Stream: new members

### Topic: How to use match expression recursively?

#### Rui Liu (Dec 24 2020 at 12:39):

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 (Dec 24 2020 at 20:04):

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 (Dec 24 2020 at 23:14):

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

Last updated: May 09 2021 at 19:11 UTC