Email Gateway (Aug 22 2022 at 14:45): Email Gateway (Aug 22 2022 at 14:45):From: "W. Douglas Maurer" <maurer@email.gwu.edu>
Some day I hope it will be possible to implement a system that does what real computers do in this case: infinity minus infinity gives NaN, which stands for Not a Number. Then any combination of NaN with anything else also gives NaN. (See any formal description of IEEE standard floating point arithmetic.) --WDMaurer
Sent from my iPhone
Email Gateway (Aug 22 2022 at 14:45):From: "Eugene W. Stark" <isabelle-users@starkeffect.com>
What will be the type of "-" in that case?
Do you really want to go there?
Email Gateway (Aug 22 2022 at 14:45):From: Lawrence Paulson <lp15@cam.ac.uk>
We do have the full IEEE model:
https://www.isa-afp.org/entries/IEEE_Floating_Point.shtml <https://www.isa-afp.org/entries/IEEE_Floating_Point.shtml>
Larry Paulson
Last updated: Apr 26 2024 at 01:06 UTC