[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