Zulip Chat Archive

Stream: general

Topic: local recursive function


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

view this post on Zulip Sebastian Ullrich (Sep 14 2018 at 15:59):

No

view this post on Zulip Sebastian Ullrich (Sep 14 2018 at 16:02):

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

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

view this post on Zulip Chris Hughes (Sep 14 2018 at 16:41):

I had to do by exact for some reason

view this post on Zulip Sebastian Ullrich (Sep 14 2018 at 16:42):

Now that's just terrible :P


Last updated: May 12 2021 at 23:13 UTC