<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=us-ascii">
<style type="text/css" style="display:none;"> P {margin-top:0;margin-bottom:0;} </style>
</head>
<body dir="ltr">
<div style="font-family: Calibri, Helvetica, sans-serif; font-size: 12pt; color: rgb(0, 0, 0);">
try `inspect (g x) y`<br>
</div>
<div style="font-family: Calibri, Helvetica, sans-serif; font-size: 12pt; color: rgb(0, 0, 0);">
<br>
</div>
<div id="signature">
<div id="divtagdefaultwrapper" dir="ltr" style="font-size:12pt; color:#000000; font-family:Calibri,Arial,Helvetica,sans-serif">
<div><font style="font-size:12pt" size="3"><span style="color:rgb(69,129,142)"><span style="font-family:trebuchet ms,sans-serif"><b>Sincerely Yours,<br>
</b></span></span></font></div>
<font style="font-size:12pt" size="3"><span style="color:rgb(69,129,142)"><span style="font-family:trebuchet ms,sans-serif"><b><br>
Jason Hu<a target="_blank"></a></b></span></span></font> </div>
</div>
<div id="appendonsend"></div>
<hr style="display:inline-block;width:98%" tabindex="-1">
<div id="divRplyFwdMsg" dir="ltr"><font face="Calibri, sans-serif" style="font-size:11pt" color="#000000"><b>From:</b> Agda <agda-bounces@lists.chalmers.se> on behalf of Xuanrui Qi <xqi01@cs.tufts.edu><br>
<b>Sent:</b> March 16, 2019 3:21 PM<br>
<b>To:</b> agda list<br>
<b>Subject:</b> [Agda] inspect idiom with more than one argument</font>
<div> </div>
</div>
<div class="BodyFragment"><font size="2"><span style="font-size:11pt;">
<div class="PlainText">Hello all,<br>
<br>
I have used the inspect idiom from time to time, but it seems that I<br>
can't really "inspect" a function call with more than 1 argument. Say I<br>
want to do this:<br>
<br>
f x y with g x y | inspect g x y<br>
<br>
However, this won't work, unfortunately. Are there any ways to work<br>
around this? e.g. uncurrying the function?<br>
<br>
Thanks,<br>
Ray<br>
<br>
-- <br>
Xuanrui (Ray) Qi<br>
<br>
xqi01@cs.tufts.edu<br>
me@xuanruiqi.com<br>
<a href="https://www.xuanruiqi.com">https://www.xuanruiqi.com</a><br>
<br>
_______________________________________________<br>
Agda mailing list<br>
Agda@lists.chalmers.se<br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</div>
</span></font></div>
</body>
</html>