I don’t intend any more changes. Fans of “approximation” may have to get used
to doing “simp add: powr_def” first.
Larry
> On 14 Apr 2015, at 15:35, Makarius wrote:
>
> Does that mean there will be further changes, to make it fully work in the
> coming release?
>
> It would be nice to see th
On Sun, 12 Apr 2015, Larry Paulson wrote:
You should always have success by unfolding powr_def. And I’m told that
the necessary changes to “approximation” are not difficult.
Does that mean there will be further changes, to make it fully work in the
coming release?
It would be nice to see th
All I know is that HOL-Codegenerator_Test failed because of some (?)
type-related ambiguity connected with powr, with no indication of where this
instance of powr actually was. Adding [code del] to its definition eliminated
the error, God knows why.
Larry
> On 12 Apr 2015, at 20:03, Florian Ha
Hi Larry,
>> * Complex powers and square roots. The functions "ln" and "powr" are now
>> overloaded for types real and complex, and 0 powr y = 0 by definition.
>> INCOMPATIBILITY: type constraints may be necessary.
>
> But I had to remove support for powr in code generation and the approximation
You should always have success by unfolding powr_def. And I’m told that the
necessary changes to “approximation” are not difficult.
Larry
> On 12 Apr 2015, at 12:26, Manuel Eberl wrote:
>
> I am not terribly happy about that. I use approximation of powr in my work on
> Akra–Bazzi and the Mast
I am not terribly happy about that. I use approximation of powr in my work on
Akra–Bazzi and the Master theorem.
I take it that a powr b = exp (ln a * b) still holds for positive a. I could
probably apply that rewrite rule before applying approximation, but it would of
course be nice if I did n
> * Complex powers and square roots. The functions "ln" and "powr" are now
> overloaded for types real and complex, and 0 powr y = 0 by definition.
> INCOMPATIBILITY: type constraints may be necessary.
But I had to remove support for powr in code generation and the approximation
method. If anybod
