[Agda] list comprehensions

[Jacques Carette]

On top of the do notation mentioned earlier, you can also do
map (λ where ((x , y) , z) → ((x , z) , y)) items

as well as
map (λ { ((x , y) , z) → ((x , z) , y) }) items

Jacques

On 2019-Dec.-10 15:04 , mechvel at scico.botik.ru wrote:
> Dear Agda developers,
>
> list comprehensions is a nice feature in Haskell.
> For example, I write
>     [((i, j), p) | ((i, p), j) <- items]
>
> to transform a list of "triples".
> But in Agda, one has to write
>     map (\item → ((proj₁ $ proj₁ item , proj₂ item) ,
>                   (proj₂ $ proj₁ item)
>                  )
>         ) items
>
> This code is difficult to perceive.
> Well, I do not know how of difficult can it be to introduce list 
> comprehensions to Agda
> (to language? to library?).
>
> Regards,
>
> ------
> Sergei
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda