[Agda] Again, a question on records

[David Leduc]

Sorry, my previous question was stupid. Here it is again, hopefully
not so stupid:

In the code below, from the type of x and y (T.carrier t), shouldn't
the type checker infer the implicit argument marked as an underscore?
Even if I put explicitly t instead of the underscore, my definition is
rejected. What is going on? What is the right way to do in Agda?

module test where

record T : Set1 where
  field carrier : Set
        op : carrier -> carrier -> carrier

[_] : T -> Set
[ t ] = T.carrier t

_$_ : {t : T} -> T.carrier t -> T.carrier t -> T.carrier t
x $ y = T.op _ x y

On Sun, Sep 19, 2010 at 2:07 PM, Jean-Philippe Bernardy
<bernardy at chalmers.se> wrote:
> On Sun, Sep 19, 2010 at 4:02 PM, David Leduc
> <david.leduc6 at googlemail.com> wrote:
>> Hi,
>>
>> I would like to introduce some notation with imolicit arguments as can
>> be done in Coq.
>> Unfortunately wen I type check the code below the underscore becomes
>> yellow (I guess it's because something is wrong).
>> If I replace the underscore by A then it does not typecheck at all.
>> How to solve this problem?
>
> From a cursory look, it seems that you should pass t, not A.
>
> Yellow means "cannot infer", which means that there could
> be other records to extract 'T.r' from.
>
> Cheers,
> JP.
>
>> module test where
>>
>> record T (A : Set) : Set1 where
>>  field r : A -> A -> A
>>
>> _$_ : {A : Set} -> {t : T A} -> A -> A -> A
>> x $ y = T.r _ x y
>> _______________________________________________
>> Agda mailing list
>> Agda at lists.chalmers.se
>> https://lists.chalmers.se/mailman/listinfo/agda
>>
>