*To*: Manuel Eberl <eberlm at in.tum.de>, isabelle-users <isabelle-users at cl.cam.ac.uk>*Subject*: Re: [isabelle] Instantiating type classes*From*: Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>*Date*: Mon, 6 Jan 2014 09:16:50 +0100*In-reply-to*: <52B22BBF.7040206@in.tum.de>*References*: <52B22BBF.7040206@in.tum.de>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:24.0) Gecko/20100101 Thunderbird/24.2.0

Hi Manuel,

Hope this helps, Andreas On 19/12/13 00:11, Manuel Eberl wrote:

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

- Previous by Date: Re: [isabelle] Where to learn about HOL vs FOL?
- Next by Date: Re: [isabelle] Easy And Language Integrated Use
- Previous by Thread: Re: [isabelle] Easy And Language Integrated Use
- Next by Thread: Re: [isabelle] isabelle build: number of threads
- Cl-isabelle-users January 2014 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list