[isabelle] Instantiating type classes
- To: isabelle-users <isabelle-users at cl.cam.ac.uk>
- Subject: [isabelle] Instantiating type classes
- From: Manuel Eberl <eberlm at in.tum.de>
- Date: Thu, 19 Dec 2013 00:11:59 +0100
- User-agent: Mozilla/5.0 (X11; Linux x86_64; rv:24.0) Gecko/20100101 Thunderbird/24.1.0
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