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

[Ulf Norell]

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
  - simple aliases: let x = e in ...
  - record unpacking: let x , y = p in ...
I'm changing the ticket to a feature request. It should be possible to also
support let f x y = e in ...

/ Ulf


On Sun, Jan 19, 2014 at 10:46 AM, Ulf Norell <ulf.norell at gmail.com> wrote:

> 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/8c380493/attachment-0001.html