Module AltErgoLib.Fpa_roundingSource

Sourceval is_rounding_mode : Expr.t -> bool
Sourceval fpa_rounding_mode : Ty.t
Sourceval _NearestTiesToEven__rounding_mode : Expr.t

ne in Gappa: to nearest, tie breaking to even mantissas

Sourceval _ToZero__rounding_mode : Expr.t

zr in Gappa: toward zero

Sourceval _Up__rounding_mode : Expr.t

up in Gappa: toward plus infinity

Sourceval _Down__rounding_mode : Expr.t

dn in Gappa: toward minus infinity

Sourceval _NearestTiesToAway__rounding_mode : Expr.t

na : to nearest, tie breaking away from zero

Sourceval _Aw__rounding_mode : Expr.t

aw in Gappa: away from zero *

Sourceval _Od__rounding_mode : Expr.t

od in Gappa: to odd mantissas

Sourceval _No__rounding_mode : Expr.t

no in Gappa: to nearest, tie breaking to odd mantissas

Sourceval _Nz__rounding_mode : Expr.t

nz in Gappa: to nearest, tie breaking toward zero

Sourceval _Nd__rounding_mode : Expr.t

nd in Gappa: to nearest, tie breaking toward minus infinity

Sourceval _Nu__rounding_mode : Expr.t

nu in Gappa: to nearest, tie breaking toward plus infinity

Sourceval integer_log_2 : Numbers.Q.t -> int

Integer part of binary logarithm for NON-ZERO POSITIVE number *

Sourceval float_of_rational : Expr.t -> Expr.t -> Expr.t -> Numbers.Q.t -> Numbers.Q.t * Numbers.Z.t * int

float_of_rational prec exp mode x float approx of a rational constant. The function also returns the mantissa and the exponent. i.e. if res, m, e = float_of_rational prec exp mode x, then res = m * 2^e *

Sourceval round_to_integer : Expr.t -> Numbers.Q.t -> Numbers.Q.t

round_to_integer mode x rounds the rational x to an integer depending on the rounding mode mode