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

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