I can refer to the fields of record instances in two ways:

Record Point := mkPoint { px : nat; py : nat }.

Definition r : Point := mkPoint 6 7.

Compute r.(px) + r.(py).

Compute (px r) + (py r).

But these fail with typeclasses:

Class PointD := mkPointD { dx : nat; dy : nat }.

Definition rd : PointD := mkPointD 6 7.

Fail Compute rd.(dx) + rd.(dy).

Fail Compute (dx rd) + (dy rd).

=> Illegal application (Non-functional construction):

The expression "dx" of type "nat" cannot be applied to the term "rd" : "PointD"

Is there a way to refer to typeclass methods or is there a basic difference here, and if so, how can I learn more about the differences? (I've looked at the Reference Manual and M. Sozeau's original papers on typeclasses.)

What if you used `@dx`

instead?

I think what happens is that when `dx`

is defined, its `PointD`

argument is automatically made implicit and since `rd.(dx)`

is another way of writing `dx rd`

the error happens (it does tell you that `dx`

is of type `nat`

).

Thank you! I missed the change to an implicit argument.

You're welcome. You can use `About dx`

or so to check this kind of thing.

Last updated: Sep 23 2023 at 07:01 UTC