[Agda] inspect idiom with more than one argument

Jason -Zhong Sheng- Hu fdhzs2010 at hotmail.com
Sat Mar 16 20:25:48 CET 2019


try `inspect (g x) y`

Sincerely Yours,

Jason Hu
________________________________
From: Agda <agda-bounces at lists.chalmers.se> on behalf of Xuanrui Qi <xqi01 at cs.tufts.edu>
Sent: March 16, 2019 3:21 PM
To: agda list
Subject: [Agda] inspect idiom with more than one argument

Hello all,

I have used the inspect idiom from time to time, but it seems that I
can't really "inspect" a function call with more than 1 argument. Say I
want to do this:

    f x y with g x y | inspect g x y

However, this won't work, unfortunately. Are there any ways to work
around this? e.g. uncurrying the function?

Thanks,
Ray

--
Xuanrui (Ray) Qi

xqi01 at cs.tufts.edu
me at xuanruiqi.com
https://www.xuanruiqi.com

_______________________________________________
Agda mailing list
Agda at lists.chalmers.se
https://lists.chalmers.se/mailman/listinfo/agda
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20190316/e6782b2d/attachment.html>


More information about the Agda mailing list