Zulip Chat Archive

Stream: new members

Topic: Meta functions with higher order variables


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
  _x_1
term has type
  ?m_1

on the first %%f.

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: Dec 20 2023 at 11:08 UTC