Re: [Agda] Weird behaviour inside of ‘let’

[Ulf Norell]

That's a straight up bug. I made a ticket:
https://code.google.com/p/agda/issues/detail?id=1028

Thanks for spotting it.

/ Ulf


On Sun, Jan 19, 2014 at 9:46 AM, Mateusz Kowalczyk
<fuuzetsu at fuuzetsu.co.uk>wrote:

> Hi,
>
> I was turning some expressions of the form ‘foo = λ a b c → f c b a’
> that I had inside a let into the ‘foo a b c = …’ form but I
> encountered a rather weird behaviour, ranging from things being
> claimed not in scope to parse errors. See [1] for some snippets. Can
> someone explain these?
>
> [1]: http://lpaste.net/98754
>
> --
> Mateusz K.
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20140119/0d64db43/attachment.html