[Agda] Again, a question on records

[Dan Doel]

On Sunday 19 September 2010 10:27:10 pm David Leduc wrote:
> Thank you for your explanation, Dan.
> But I want that the infix notation _$_ works for all record of type T.
> More precisely, how can I translate the following Coq code in Agda?
> 
> Record T : Type := {
>   carrier : Set ;
>   op : carrier -> carrier -> carrier
> }.
> 
> Notation "[ t ]" := (carrier t).
> 
> Notation "x $ y" := (op _ x y) (at level 50, left associativity).
> 
> Definition f (t1 t2 : T)(x1 y1: [t1])(x2 y2:[t2]) : [t1]*[t2] :=
>   (x1 $ y1, x2 $ y2).
> 
> You see here that the right record is inferred from the types of xi and y1.

Ah, right. The $s will still be yellow because the record they go with can't 
be inferred for the same reason that the _ can't be inferred in the definition 
of _$_.

I don't think there's much you can do at present. I'm not sure how Coq does 
it, either. I guess it just makes (pretty reasonable) assumption that t should 
be filled in for the operations on [t]?