[Agda] Location of implicit argument(s)

[Dan Licata]

In Twelf, you can specify implicit arguments by giving a type
annotation; e.g. you could write 
foo (x : Zomg) bar y for foo_bar_ {Zomg} x y 
(except Twelf doesn't have mixfix to begin with).

I often find myself wishing for this in Agda; e.g. when I have

Lam : forall {G A B} -> Term (A :: G) B -> Term G (A imp B)

I want to write

f (Lam (e : Term (A :: G) B)) = ...

for

f (Lam{G}{A}{B} e) = ...

The reason is that the former saves me from having to remember what
order the implicit arguments come in (when there's a lot of them, I have
to keep flipping back to the definition of the datatype).

Could such a syntax be made to work for Agda?

-Dan




On Nov20, Dirk Ullrich 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?
> >
> > 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
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>