local recursive function

Stream: general

[Reid Barton]

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

[Sebastian Ullrich]

No

[Sebastian Ullrich]

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

[Chris Hughes]

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]

I had to do by exact for some reason

[Sebastian Ullrich]

Now that's just terrible :P