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
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
Perhaps this should be put in the library?
This archive was generated by a fusion of
Pipermail (Mailman edition) and