[Agda] Location of implicit argument(s)

[Dan Licata]

Thanks Jean-Philippe and Darin -- that trick works nicely in
expressions.  However, the spot where I really want this syntax is in
*patterns* (to name the implicit args to a function, or to a constructor
argument to a function). Is there a trick to do that?

You can't write

  f : forall {n} -> Vec n -> Vec n
  f (x : Vec n) = ...

as

  data Typed : Set1 where
    _has_ : (A : Set) -> A -> Typed

  f : forall {n} -> Vec n -> Vec n
  f x with _ has x
  ...    | ((Vec n) has x') = {!!}

because you can't pattern-match on Sets.  Though I suppose this would
work for types in a universe, because you could match on the codes.

-Dan

On Nov20, Darin Morrison wrote:
> 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
>