Mark Wassell (Nov 28 2021 at 08:57): Mark Wassell (Nov 28 2021 at 08:57):I would like to define a subclass and specify that there must be at least two members satisfying a property. So I have:
definition myP :: "'a :: ab_group_add ⇒ 'a ⇒ bool" where
"myP x y = True"
class myclass = ab_group_add +
fixes p1 and p2
assumes myclass_pred : "myP p1 p2"
but I get
Type inference imposes additional sort constraint ab_group_add of type parameter 'a of sort type
My impression is that p1 and p2 are members of myclass, so are members of ab_group_add and myP p1 p2 should type check.
Mark
Lukas Stevens (Nov 28 2021 at 12:54):This is kind of tricky. In the context of a type class on some type 'a you actually don't have the fact available that 'a is of that class. You only get the relevant assumptions about the type, e.g. that + is available. What you can do is to put your definition inside the context of the class:
definition (in ab_group_add) myP :: "'a ⇒ 'a ⇒ bool" where
"myP x y = True"
class myclass = ab_group_add +
fixes p1 and p2
assumes myclass_pred : "myP p1 p2
Note that the 'a in the definition of myP refers to the type that the class ab_group_add works on.
Last updated: Dec 21 2024 at 16:20 UTC