[Agda] A question on records

[Jean-Philippe Bernardy]

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
>