[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