package coq-core

  1. Overview
  2. Docs
package coq-core
Legend:
Library
Module
Module type
Parameter
Class
Class type
type t

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.

val is_nan : t -> bool

Test functions for special values to avoid calling classify

val is_infinity : t -> bool
val is_neg_infinity : t -> bool
val of_string : string -> t
val 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).

val 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.

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

All NaNs are normalized to Stdlib.nan.

  • since 8.15
val sign : t -> bool

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

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

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

type float_class =
  1. | PNormal
  2. | NNormal
  3. | PSubn
  4. | NSubn
  5. | PZero
  6. | NZero
  7. | PInf
  8. | NInf
  9. | NaN
val classify : t -> float_class
val mul : t -> t -> t
val add : t -> t -> t
val sub : t -> t -> t
val div : t -> t -> t
val sqrt : t -> t
val of_uint63 : Uint63.t -> t

Link with integers

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

Shifted exponent extraction

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

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

val hash : t -> int
val total_compare : t -> t -> int

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

val 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