diff options
Diffstat (limited to 'kernel/float64.mli')
| -rw-r--r-- | kernel/float64.mli | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/kernel/float64.mli b/kernel/float64.mli index 927594115e..acc3a556ab 100644 --- a/kernel/float64.mli +++ b/kernel/float64.mli @@ -14,6 +14,7 @@ Beware: NaNs have a sign and a payload, while they should be indistinguishable from Coq's perspective. *) type t +(** Test functions for special values to avoid calling [classify] *) val is_nan : t -> bool val is_infinity : t -> bool val is_neg_infinity : t -> bool @@ -25,6 +26,9 @@ val compile : t -> string val of_float : float -> t +(** Return [true] for "-", [false] for "+". *) +val sign : t -> bool + val opp : t -> t val abs : t -> t |