*To*: Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>, "cl-isabelle-users at lists.cam.ac.uk" <cl-isabelle-users at lists.cam.ac.uk>*Subject*: Re: [isabelle] Code equations for "power"*From*: Manuel Eberl <eberlm at in.tum.de>*Date*: Fri, 8 Jan 2016 17:26:11 +0100*In-reply-to*: <568FE115.4040500@inf.ethz.ch>*References*: <568FCF40.30901@in.tum.de> <568FE115.4040500@inf.ethz.ch>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:38.0) Gecko/20100101 Thunderbird/38.5.0

The code_unfold works if the call to power in the code equations istypes with something of sort mult_monoid. So if the code equation usespower on one of the standard numeric types, everything is fine. But ifyou use power polymorphically for some 'a, then this does not work ifmult_monoid is not a supersort of 'a's sort. For example, if you havesomething like

Perhaps this should be put in the library? Cheers, Manuel

**Follow-Ups**:**Re: [isabelle] Code equations for "power"***From:*Andreas Lochbihler

**References**:**[isabelle] Code equations for "power"***From:*Manuel Eberl

**Re: [isabelle] Code equations for "power"***From:*Andreas Lochbihler

- Previous by Date: Re: [isabelle] Isabelle2016-RC0: Windows bootstrapping
- Next by Date: Re: [isabelle] Code equations for "power"
- Previous by Thread: Re: [isabelle] Code equations for "power"
- Next by Thread: Re: [isabelle] Code equations for "power"
- Cl-isabelle-users January 2016 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