[Agda] list comprehensions

[mechvel at scico.botik.ru]

On 2019-12-11 13:48, mechvel at scico.botik.ru wrote:
> On 2019-12-11 02:55, James Wood wrote:
>> Dear Sergei,
>> 
>> [..]
>> 
> 
>> The most direct is the `λ where` syntax, that allows pattern matching.
>> 
>>   map (λ where ((i , p) , j) → ((i , j) , p)) items
>> 
>> This can cause issues when you want to repeat this expression 
>> somewhere
>> else, in which case you can rewrite to something more verbose.
>> 
>>   map (λ item → let ((i , p) , j) = item in ((i , j) , p)) items
>> 
>> I believe in the development version of Agda, it's even possible to
>> write the following.
>> 
>>   map (λ ((i , p) , j) → ((i , j) , p)) items
> 

> Any of this will do.
> [..]


And the latter version is much nicer.

--
SM