Re: [isabelle] Instantiating type classes
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