[isabelle] Instantiating type classes


I have some type class foo that fixes some function f: 'a => 'a:

class foo = fixes f :: "'a => 'a"

Now suppose, for instance, that if I have a monoid, I can provide such
an f. Is it possible to have any monoid automatically by a "foo" as
well, if I give a construction of the function f for any monoid?

I cannot simply delete the class foo and put f directly into monoid,
because I also want to be able to provide some types with such a
function f that are not monoids.


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.