diff options
| author | Pierre Roux | 2020-03-31 19:12:18 +0200 |
|---|---|---|
| committer | Pierre Roux | 2020-05-19 12:05:29 +0200 |
| commit | 04e22abe4378e29671def7b4d9c7e509c58ef6b6 (patch) | |
| tree | 3cafb2ad562d0472e115225eeb7848b7ec8cdbd2 /kernel/float64.mli | |
| parent | a5c9ad83071c99110fed464a0b9a0f5e73f1be9b (diff) | |
[primitive floats] Add low level hexadecimal printing
Diffstat (limited to 'kernel/float64.mli')
| -rw-r--r-- | kernel/float64.mli | 12 |
1 files changed, 11 insertions, 1 deletions
diff --git a/kernel/float64.mli b/kernel/float64.mli index d43ff4553f..0afbfa89da 100644 --- a/kernel/float64.mli +++ b/kernel/float64.mli @@ -19,9 +19,19 @@ val is_nan : t -> bool val is_infinity : t -> bool val is_neg_infinity : t -> bool -val to_string : t -> string val of_string : string -> t +(** Print a float exactly as an hexadecimal value (exact decimal + * printing would be possible but sometimes requires more than 700 + * digits). *) +val to_hex_string : t -> string + +(** Print a float as a decimal value. The printing is not exact (the + * real value printed is not always the given floating-point value), + * however printing is precise enough that forall float [f], + * [of_string (to_decimal_string f) = f]. *) +val to_string : t -> string + val compile : t -> string val of_float : float -> t |
