[Agda] Location of implicit argument(s)

[Dirk Ullrich]

Hi,

first of all I want to say that I am very excited by 'implemented type
theoroes' like Agda: It lives at the borderline of two of my favorite
subjects, (constructive) logic and programming.

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