## Stream: general

### Topic: local recursive function

#### Reid Barton (Sep 14 2018 at 15:05):

Can you define a recursive function with a let inside a do block (in a meta definition)?

No

#### Sebastian Ullrich (Sep 14 2018 at 16:02):

Well, you could write a meta fix, but that's still not very ergonomical

#### Chris Hughes (Sep 14 2018 at 16:41):

meta def foo (n : ℕ) : option ℕ :=
do let m : ℕ :=
match n with
| 0     := 1
| (n+1) := by exact _match n + _match n
end,
return m

#eval foo 4 -- some 16


#### Chris Hughes (Sep 14 2018 at 16:41):

I had to do by exact for some reason

#### Sebastian Ullrich (Sep 14 2018 at 16:42):

Now that's just terrible :P

Last updated: May 12 2021 at 23:13 UTC