Stream: Beginner Questions

Topic: Defining class with at least two members satisfying property


view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Lukas Stevens (Nov 28 2021 at 12:55):

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