Stream: new members
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