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

Hi Manuel, On 08/01/16 17:26, Manuel Eberl wrote:

The code_unfold works if the call to power in the code equations is types with something of sort mult_monoid. So if the code equation uses power on one of the standard numeric types, everything is fine. But if you use power polymorphically for some 'a, then this does not work if mult_monoid is not a supersort of 'a's sort. For example, if you have something likeI guess that's a pretty good compromise, isn't it? Most of the time, exported code using the "power" operation will probably be dealing with types that fulfil at least monoid_mult, and then this fast variant could be used.

Best, Andreas

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

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

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

- Previous by Date: Re: [isabelle] Code equations for "power"
- Next by Date: Re: [isabelle] Isabelle2016-RC0: symbols sometimes displayed as ASCII strings
- 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