Re: [isabelle] Instantiating type classes

Hi Manuel,

no, there is currently no such mechanism to automatically propagate type class instantiations. The same issue appears in the HOL library for topologic spaces generated from other structures (e.g. class order_topology in ~~/src/HOL/Topological_Spaces.thy), too; separate type classes explicitly *assume* that the open sets are equal to some construction. Maybe, a similar solution can work for you, too.

Hope this helps,

On 19/12/13 00:11, Manuel Eberl wrote:

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.