You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Add proofs of the following floating point theorems:
!x . not float_equal x x <=> float_is_nan x
!x . float_unordered x x <=> float_is_nan x
!x . (float_equal x (float_plus_infinity (:'t # 'w))) \/ (float_equal x (float_minus_infinity (:'t # 'w))) <=> float_is_infinite x;
!x . float_equal x (float_plus_zero (:'w # 't)) <=> float_is_zero x
These theorems prove that the typical implementations of fp_is_nan etc. (if you don't have fp_classify) are correct.
The text was updated successfully, but these errors were encountered:
The third one of these theorems is closely related to float_infinities in binary_ieeeScript.sml. The critical difference is that it uses float_equal rather than =.
(testing for x = float_minus_infinity is equivalent to testing for float_equal x float_minus_infinity, but you need to prove that)
(Feature request)
Add proofs of the following floating point theorems:
These theorems prove that the typical implementations of fp_is_nan etc. (if you don't have fp_classify) are correct.
The text was updated successfully, but these errors were encountered: