[Agda] Location of implicit argument(s)

Ulf Norell ulfn at chalmers.se
Fri Nov 20 10:27:45 CET 2009


On Fri, Nov 20, 2009 at 9:34 AM, Dirk Ullrich
<dirk.ullrich at googlemail.com>wrote:

> Hi,
>
> 2009/11/20 Daniel Peebles <pumpkingod at gmail.com>:
> > The only way I know of is to write the function without using the
> > mixfix-ness, as foo_bar_ {Zomg} x y.
> Thanks, David - I have tried this and it works.
> But is there only a way with using mixfix-ness?


There is no way to give the implicit arguments and still retain the
mixfixiness.

/ Ulf
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20091120/82e06a75/attachment-0001.html


More information about the Agda mailing list