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.
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: Jul 15 2022 at 23:21 UTC