[Agda] list comprehensions
mechvel at scico.botik.ru
mechvel at scico.botik.ru
Tue Dec 10 21:04:02 CET 2019
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
More information about the Agda
mailing list