diff options
| -rw-r--r-- | lib/IEEE754_extra.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/lib/IEEE754_extra.v b/lib/IEEE754_extra.v index 83cacb2b..56b90727 100644 --- a/lib/IEEE754_extra.v +++ b/lib/IEEE754_extra.v @@ -1014,7 +1014,7 @@ Proof. rewrite plus_IZR. lra. Qed. - + Theorem ZofB_ne_correct: forall f, ZofB_ne f = if is_finite _ _ f then Some (ZnearestE (B2R _ _ f)) else None. |