<div dir="ltr">Actually, looking at the code we never supported the let f x = ... form without a type signature for f (which can be f : _). The things you can say in a let without giving a type signature are<div> - simple aliases: let x = e in ...</div>
<div> - record unpacking: let x , y = p in ...</div><div>I'm changing the ticket to a feature request. It should be possible to also support let f x y = e in ...</div><div><br></div><div>/ Ulf</div></div><div class="gmail_extra">
<br><br><div class="gmail_quote">On Sun, Jan 19, 2014 at 10:46 AM, Ulf Norell <span dir="ltr"><<a href="mailto:ulf.norell@gmail.com" target="_blank">ulf.norell@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
<div dir="ltr">That's a straight up bug. I made a ticket: <a href="https://code.google.com/p/agda/issues/detail?id=1028" target="_blank">https://code.google.com/p/agda/issues/detail?id=1028</a><div><br></div><div>Thanks for spotting it.</div>
<span class="HOEnZb"><font color="#888888">
<div><br></div><div>/ Ulf</div></font></span></div><div class="HOEnZb"><div class="h5"><div class="gmail_extra"><br><br><div class="gmail_quote">On Sun, Jan 19, 2014 at 9:46 AM, Mateusz Kowalczyk <span dir="ltr"><<a href="mailto:fuuzetsu@fuuzetsu.co.uk" target="_blank">fuuzetsu@fuuzetsu.co.uk</a>></span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Hi,<br>
<br>
I was turning some expressions of the form ‘foo = λ a b c → f c b a’<br>
that I had inside a let into the ‘foo a b c = …’ form but I<br>
encountered a rather weird behaviour, ranging from things being<br>
claimed not in scope to parse errors. See [1] for some snippets. Can<br>
someone explain these?<br>
<br>
[1]: <a href="http://lpaste.net/98754" target="_blank">http://lpaste.net/98754</a><br>
<br>
--<br>
Mateusz K.<br>
_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</blockquote></div><br></div>
</div></div></blockquote></div><br></div>