Re: [isabelle] Code equations for "power"



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 like

I 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.

Perhaps this should be put in the library?


Cheers,

Manuel




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.