[Agda] (\ x , e → x ^ e)

Matus Tejiscak ziman at functor.sk
Tue Dec 10 19:51:09 CET 2013


Hello,

Yes, there is:
> map λ { (x , e) → x ^ e }

Or, alternatively:
> map (uncurry _^_)

The expression "x , e" as an application of a constructor so you need  
the pattern-matching lambda to deconstruct it.

Matus
-------------- next part --------------
A non-text attachment was scrubbed...
Name: not available
Type: application/pgp-signature
Size: 490 bytes
Desc: PGP Digital Signature
Url : http://lists.chalmers.se/pipermail/agda/attachments/20131210/5f4af47d/attachment.bin


More information about the Agda mailing list