[Agda] pair list in lib ?

[Twan van Laarhoven]

On 06/11/13 12:11, 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:
>
> ..

I just realized that this function is actually built in to Applicative:

     pairs : ∀ {A B : Set} → List A → List B → List (A × B)
     pairs = RawMonad._⊗_ Data.List.monad
     -- or equivalently
     pairs = _⊗_  where open RawMonad Data.List.monad


Twan