Email Gateway (Aug 19 2022 at 13:04): Email Gateway (Aug 19 2022 at 13:04):From: Manuel Eberl <eberlm@in.tum.de>
Hallo,
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.
Cheers,
Manuel
Email Gateway (Aug 19 2022 at 13:29):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
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,
Andreas
Last updated: Apr 16 2024 at 16:19 UTC