mathlib documentation

core.init.meta.float

meta constant native.float  :
Type

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: https://en.cppreference.com/w/cpp/types/numeric_limits/epsilon

returns the maximum rounding error

Positive infinity.

meta constant native.float.qNaN  :

Quiet NaN.

meta constant native.float.sNaN  :

Signalling NaN.

meta constant native.float.is_infinite (a : native.float) :

Returns true when the value is positive or negative infinity.

meta constant native.float.is_nan (a : native.float) :

Returns true when the value is qNaN or sNaN

meta constant native.float.is_normal (a : native.float) :

Reference: https://en.cppreference.com/w/cpp/numeric/math/isnormal https://stackoverflow.com/questions/8341395/what-is-a-subnormal-floating-point-number

meta constant native.float.sign (a : native.float) :

The sign s of the float. tt if negative.

meta constant native.float.exponent (a : native.float) :

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

meta constant native.float.add (a a_1 : native.float) :

@[instance]

meta constant native.float.sub (a a_1 : native.float) :

@[instance]

@[instance]

meta constant native.float.mul (a a_1 : native.float) :

@[instance]

meta constant native.float.div (a a_1 : native.float) :

@[instance]

meta constant native.float.fmod (a a_1 : native.float) :

remainder of the floating point division operation.

meta constant native.float.remainder (a a_1 : native.float) :

signed remainder of the division operation.

meta constant native.float.max (a a_1 : native.float) :

meta constant native.float.min (a a_1 : native.float) :

meta constant native.float.pow (a a_1 : native.float) :

Square root.

Cube root.

meta constant native.float.hypot (a a_1 : native.float) :

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

meta constant native.float.exp (a : native.float) :

Exponential function.

2 raised to the given power.

meta constant native.float.log (a : native.float) :

Natural logarithm.

meta constant native.float.pi  :

meta constant native.float.atan2 (a a_1 : native.float) :

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

meta constant native.float.ceil (a : native.float) :

Nearest integer not less than the given value.

meta constant native.float.floor (a : native.float) :

Nearest integer not greater than the given value.

meta constant native.float.trunc (a : native.float) :

Nearest integer not greater in magnitude than the given value.

meta constant native.float.round (a : native.float) :

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

meta constant native.float.lt (a a_1 : native.float) :

@[instance]

meta constant native.float.le (a a_1 : native.float) :

@[instance]

@[instance]

meta constant native.float.of_nat (a : ) :

meta constant native.float.of_int (a : ) :

@[instance]