[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