[Agda] list comprehensions

[mechvel at scico.botik.ru]

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. Thank you.
Sorry, I must have recalled this myself.

--
SM