[Agda] pair list in lib ?
mechvel at botik.ru
Wed Nov 6 14:53:10 CET 2013
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.
More information about the Agda