Hi Manual,
thanks for your efforts, but I believe there is already a more efficient way to
compute log2.
In your implementation, consider your intlog2_aux which roughly requires y
iterations if log2(x) = y,
since you always just add 1 to the accumulator.
For some of my applications this
Hi Manuel,
You are not the first to encouter this problem. Here's my experience:
In 4b1b85f38944, I added code_printings for gcd and decided to add Gcd to the imports of
Code_Target_Nat. IIRC this broke a few things in the AFP, which I had to fix. Meanwhile,
Gcd has become part of Main again.
Hallo,
I'm considering adding efficient code for Discrete.log (the dual
logarithm on natural numbers). PolyML does provide an IntInf.log2
function that seems reasonably efficient so that one can set up code
printing. However, I am struggling with one detail:
Where would the code that does this
