[Agda] (\ x , e → x ^ e)
Sergei Meshveliani
mechvel at botik.ru
Tue Dec 10 19:29:12 CET 2013
People,
For pairs : List (C × ℕ), _^_ : C -> ℕ -> C,
it works
prims : List C
prims = zipWith _^_ (map proj₁ pairs) (map proj₂ pairs) -- (1)
I thought that
prims = map (\ x , e → x ^ e) pairs
looks better.
But the checker (development November 2013, MAlonzo) reports
(Data.Product.Σ C (λ x → ℕ)) !=< C of type (Set α)
when checking that the expression pairs has type List C
If I set map (\ (x , e) -> x ^ e) pairs
then it is not parsed.
Is there possible something nicer than (1) ?
Thanks,
------
Sergei
More information about the Agda
mailing list