[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