[Agda] Weird behaviour inside of ‘let’

[Mateusz Kowalczyk]

On 19/01/14 09:58, Ulf Norell wrote:
> 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
>>>
>>
>>
> 

Ah great, it'll be a welcome enhancement. Can you explain what's
happening when Agda sees

f x y z = y

Is it trying to do record unpacking or something along these lines? The
‘not in scope’ message is rather uninformative and I'm rather interested
what it's trying to do. Perhaps it's trying to unpack on some (possible)
mixfix, but that's just a guess.

-- 
Mateusz K.