Library Coq.Floats.PrimFloat
Definition of the interface for primitive floating-point arithmetic
This interface provides processor operators for the Binary64 format of the
IEEE 754-2008 standard.
Type definition for the co-domain of compare
The main type
float: primitive type for Binary64 floating-point numbers.
Delimit Scope float_scope with float.
Notation "- x" := (
opp x) :
float_scope.
Notation "x == y" := (
eqb x y) (
at level 70,
no associativity) :
float_scope.
Notation "x < y" := (
ltb x y) (
at level 70,
no associativity) :
float_scope.
Notation "x <= y" := (
leb x y) (
at level 70,
no associativity) :
float_scope.
Notation "x ?= y" := (
compare x y) (
at level 70,
no associativity) :
float_scope.
Notation "x * y" := (
mul x y) :
float_scope.
Notation "x + y" := (
add x y) :
float_scope.
Notation "x - y" := (
sub x y) :
float_scope.
Notation "x / y" := (
div x y) :
float_scope.
Conversions
of_int63: convert a primitive integer into a float value.
The value is rounded if need be.
Specification of
normfr_mantissa:
- If the input is a float value with an absolute value inside [0.5, 1.);
- Then return its mantissa as a primitive integer.
The mantissa will be a 53-bit integer with its most significant bit set to 1;
- Else return zero.
The sign bit is always ignored.
Exponent manipulation functions
frshiftexp: convert a float to fractional part in [0.5, 1.)
and integer part.
ldshiftexp: multiply a float by an integral power of 2.
Predecesor/Successor functions
next_up: return the next float towards positive infinity.
next_down: return the next float towards negative infinity.
Special values (needed for pretty-printing)
Definition infinity :=
Eval compute in div (
of_int63 1) (
of_int63 0).
Definition neg_infinity :=
Eval compute in opp infinity.
Definition nan :=
Eval compute in div (
of_int63 0) (
of_int63 0).
Definition one :=
Eval compute in (
of_int63 1).
Definition zero :=
Eval compute in (
of_int63 0).
Definition neg_zero :=
Eval compute in (
-zero)%
float.
Definition two :=
Eval compute in (
of_int63 2).
Predicates and helper functions
get_sign: return true for - sign, false for + sign.