Zulip Chat Archive

Stream: new members

Topic: How to use match expression recursively?

view this post on Zulip 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.

view this post on Zulip 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
#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.

view this post on Zulip Rui Liu (Dec 24 2020 at 23:14):

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

Last updated: May 09 2021 at 19:11 UTC