Meta functions with higher order variables

Stream: new members

[Ken Roe]

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]

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