[Agda] pair list in lib ?

[Sergei Meshveliani]

On Wed, 2013-11-06 at 12:11 +0000, Twan van Laarhoven wrote:
> 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
> 

Thank you. I had 1 line more for it.
My idea was that if Standard library has an item, it is better to import
it, even if it is of 1 line. 

Regards,

------
Sergei