Zulip Chat Archive

Stream: new members

Topic: Meta functions with higher order variables

view this post on Zulip Ken Roe (Jul 28 2018 at 22:42):

How can I get the following to parse:

meta def test : expr  expr
| `(λ s, %%f s) := `(λ s, %%f (s+1))
| x := x.

Currently, I'm getting the error:

function expected at
term has type

on the first %%f.

view this post on Zulip Sebastian Ullrich (Jul 29 2018 at 02:21):

You should use an explicit type annotation (%%f : ...) s. Though if you don't statically know the type, you shouldn't use expr quotations.

Last updated: May 14 2021 at 22:15 UTC