package coq

  1. Overview
  2. Docs
package coq
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module Float64_commonSource

Sourcetype t = float

t is currently implemented by OCaml's float type.

Beware: NaNs have a sign and a payload, while they should be indistinguishable from Coq's perspective.

Sourceval is_nan : t -> bool

Test functions for special values to avoid calling classify

Sourceval is_infinity : t -> bool
Sourceval is_neg_infinity : t -> bool
Sourceval of_string : string -> t
Sourceval to_hex_string : t -> string

Print a float exactly as an hexadecimal value (exact decimal * printing would be possible but sometimes requires more than 700 * digits).

Sourceval to_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.

Sourceval compile : t -> string
Sourceval of_float : float -> t
Sourceval to_float : t -> float

All NaNs are normalized to Stdlib.nan. *

  • since 8.15
Sourceval sign : t -> bool

Return true for "-", false for "+".

Sourceval opp : t -> t
Sourceval abs : t -> t
Sourcetype float_comparison =
  1. | FEq
  2. | FLt
  3. | FGt
  4. | FNotComparable
Sourceval eq : t -> t -> bool
Sourceval lt : t -> t -> bool
Sourceval le : t -> t -> bool
Sourceval compare : t -> t -> float_comparison

The IEEE 754 float comparison. * NotComparable is returned if there is a NaN in the arguments

Sourcetype float_class =
  1. | PNormal
  2. | NNormal
  3. | PSubn
  4. | NSubn
  5. | PZero
  6. | NZero
  7. | PInf
  8. | NInf
  9. | NaN
Sourceval classify : t -> float_class
Sourceval of_uint63 : Uint63.t -> t

Link with integers

Sourceval normfr_mantissa : t -> Uint63.t
Sourceval eshift : int

Shifted exponent extraction

Sourceval frshiftexp : t -> t * Uint63.t
Sourceval ldshiftexp : t -> Uint63.t -> t
Sourceval next_up : t -> t
Sourceval next_down : t -> t
Sourceval equal : t -> t -> bool

Return true if two floats are equal. * All NaN values are considered equal.

Sourceval hash : t -> int
Sourceval total_compare : t -> t -> int

Total order relation over float values. Behaves like Pervasives.compare.

Sourceval is_float64 : Obj.t -> bool
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct