[Agda] Location of implicit argument(s)

[Dirk Ullrich]

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?
>
> On Thu, Nov 19, 2009 at 8:00 PM, Dirk Ullrich
> <dirk.ullrich at googlemail.com> wrote:
[..]
>> I have a newbie question: If I define an mixfix function with implicit
>> argument(s) - say
>> foo_bar_ : {T : Set} -> T -> T -> T
>> where I can give the implicit argument if I want / need that?
>>

Dirk