[Agda] Location of implicit argument(s)

[Darin Morrison]

On 20 Nov 2009, at 12:03, Dan Licata wrote:

> 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

I think this function from the standard library might do what you want:

http://www.cs.nott.ac.uk/~nad/listings/lib-0.2/Data.Function.html#2782

Cheers,
Darin

This message has been checked for viruses but the contents of an attachment
may still contain software viruses, which could damage your computer system:
you are advised to perform your own checks. Email communications with the
University of Nottingham may be monitored as permitted by UK legislation.