[Agda] Location of implicit argument(s)

[Daniel Peebles]

The only way I know of is to write the function without using the
mixfix-ness, as foo_bar_ {Zomg} x y.

On Thu, Nov 19, 2009 at 8:00 PM, Dirk Ullrich
<dirk.ullrich at googlemail.com> wrote:
> 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
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>