## 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: May 14 2021 at 22:15 UTC