package rocq-runtime
Install
Dune Dependency
Authors
Maintainers
Sources
md5=8d522602d23e7a665631826dab9aa92b
sha512=f4f76a6a178e421c99ee7a331a2fd97a06e9c5d0168d7e60c44e3820d8e1a124370ea104ad90c7f87a9a1e9d87b2d0d7d2d387c998feeaed4a75ed04e176a4be
doc/rocq-runtime.kernel/Float64/index.html
Module Float64
Source
t
is currently implemented by OCaml's float
type.
Beware: NaNs have a sign and a payload, while they should be indistinguishable from Rocq's perspective.
Print a float exactly as an hexadecimal value (exact decimal * printing would be possible but sometimes requires more than 700 * digits).
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
.
The IEEE 754 float comparison. * NotComparable is returned if there is a NaN in the arguments
Shifted exponent extraction
Return true if two floats are equal. * All NaN values are considered equal.
Total order relation over float values. Behaves like Pervasives.compare
.