[Agda] inspect idiom with more than one argument

Xuanrui Qi xqi01 at cs.tufts.edu
Sat Mar 16 21:27:04 CET 2019


Oops. Of course this works.

Thanks a lot,
Ray

On Sat, 2019-03-16 at 19:25 +0000, Jason -Zhong Sheng- Hu wrote:
> 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
> 



More information about the Agda mailing list