[Afp-submit] AFP entry Neural_Networks

[Lawrence Paulson]

I know that converting a floating point number to decimal notation is tricky, but we must've had correct algorithms for decades now. I wonder whether anybody has formalised one :-)

Larry
On 20 Nov 2025 at 13:21 +0000, Achim D. Brucker <adbrucker at 0x5f.org>, wrote:

This is also my assumption.  The values used by me in the below example
are after pretty printing (i.e., convertio to strings).

The actually value stored is 0.070820772089064121246337890625 (decoding
it "manually", following the standard). Trying to print it in a small C
programm gives 0.00708207720890641212, which seems to be the offical
decimal represenation according to the standard. IEEE754  is not easy ...
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20251120/9eb4c720/attachment.htm>