Stream: new members
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