mathlib documentation

core / init.meta.float

meta constant native.float  :

The base. Either 2 or 10.

The length of the mantissa.

The maximum exponent.

The minimum exponent. = 1 - emax

Returns the difference between 1.0 and the next representable value of the given floating-point type. Reference:

returns the maximum rounding error

Positive infinity.

meta constant native.float.qNaN  :

Quiet NaN.

meta constant native.float.sNaN  :

Signalling NaN.

Returns true when the value is positive or negative infinity.

meta constant native.float.is_nan  :

Returns true when the value is qNaN or sNaN

meta constant native.float.sign  :

The sign s of the float. tt if negative.

The exponent e of the float in the base given by radix. emin ≤ e ≤ emax. Returns none if the number is not finite.

Decompose the number f in to (s,e) where 0.5 ≤ s < 1.0 and emin ≤ e ≤ emax such that f = s * 2 ^ e.

Decompose in to integer fst and fractional snd parts.

mantissa f returns a number s where 0.5 ≤ s < 1.0 such that there exists an integer e such that f = s * 2 ^ e


remainder of the floating point division operation.

signed remainder of the division operation.

Square root.

Cube root.

Computes sqrt(x^2 + y^2).

Exponential function.

2 raised to the given power.

Natural logarithm.

meta constant native.float.pi  :

atan2 y x finds the angle anticlockwise from the x-axis to the point [x,y].

meta constant native.float.ceil  :

Nearest integer not less than the given value.

meta constant native.float.floor  :

Nearest integer not greater than the given value.

meta constant native.float.trunc  :

Nearest integer not greater in magnitude than the given value.

meta constant native.float.round  :

Round to the nearest integer, rounding away from zero in halfway cases.

meta constant native.float.of_nat  :
meta constant native.float.of_int  :