<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">https://code.google.com/p/agda/issues/detail?id=1028</a><div><br></div><div>Thanks for spotting it.</div>
<div><br></div><div>/ Ulf</div></div><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">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>