Module positive_difference 

positive_difference_prec_round and related functions, for computing positive differences of Floats.

Functions

primitive_float_positive_difference

Computes the positive difference of two primitive floats — $x-y$ if $x>y$, and $+0.0$ otherwise — using emulated Float arithmetic.

primitive_float_positive_difference_rational

Computes the positive difference of a primitive float and a Rational — $x-y$ if $x>y$, and $+0.0$ otherwise — correctly rounding the result to the nearest value.

primitive_float_rational_positive_difference_float

Computes the positive difference of a Rational and a primitive float — $x-y$ if $x>y$, and $+0.0$ otherwise — correctly rounding the result to the nearest value.