[Agda] pair list in lib ?

Twan van Laarhoven twanvl at gmail.com
Wed Nov 6 13:11:02 CET 2013


On 05/11/13 18:22, Sergei Meshveliani wrote:
> Please, what  lib-0.7  has for the pair list ?
> The one which in Haskell is expressed as
>
>      \ xs ys -> [(x , y) | x <- xs , y <- ys]

In Haskell this desugars to uses of concatMap. You can write the same desugared 
code in Agda with the functions from Data.List:

     \xs ys -> concatMap (\x -> concatMap (\y -> [ x , y ]) ys) xs

or the shorter

     \xs ys -> concatMap (\x -> map (_,_ x) ys) xs


Twan


More information about the Agda mailing list