Rich Hilliard (Aug 22 2021 at 17:22): Rich Hilliard (Aug 22 2021 at 17:22):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.)
Théo Winterhalter (Aug 22 2021 at 17:26):What if you used @dx instead?
Théo Winterhalter (Aug 22 2021 at 17:27):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).
Rich Hilliard (Aug 22 2021 at 17:37):Thank you! I missed the change to an implicit argument.
Théo Winterhalter (Aug 22 2021 at 17:39):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