~/bend-docscommunity

spec/math/f64.bend checks

raw source on the hub · import bend-collections-laws-math@1.0.0.0/spec/math/f64.bend as F64

7 imports
import Base
import ../lib/common.bend as C
import ../../src/math/f64.bend as F
import ../../src/math/natural.bend as M
import ../../src/math/u64.bend as WU
import ../../src/math/num.bend as N
import ./w64.bend as SW

Types

type Rat source · line 574 · raw

Data

(sign, numerator, exponent of the denominator)

Definitions

def hi_nat source · line 70 · raw

@x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> Nat

def lo_nat source · line 73 · raw

@x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> Nat

def sign source · line 77 · raw

@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> Bool

bit 63, bits 52..62 and bits 0..51 of the pattern

def efield source · line 80 · raw

@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> Nat

def frac source · line 83 · raw

@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> Nat

def b2n source · line 86 · raw

@b:Bool -> Nat

def encode source · line 95 · raw

@+s:Bool -> @+ef:Nat -> @+f:Nat -> 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64

the double with sign s, exponent field ef < 2^11 and fraction f < 2^52: (s * 2^11 + ef) * 2^52 + f

def pick source · line 98 · raw

@-T:Data -> @c:Bool -> @+a:T -> @+b:T -> T

def pickt source · line 106 · raw

@-T:Type -> @c:Bool -> @a:T -> @b:T -> T

pick for pairs (a Sigma is Type-sorted)

def qnan source · line 114 · raw

0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64

encode(False, 2047, 2^51), encode(s, 2047, 0) and encode(s, 0, 0)

def inf source · line 117 · raw

@+s:Bool -> 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64

def zero source · line 120 · raw

@+s:Bool -> 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64

def is_nan source · line 123 · raw

@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> Bool

def is_inf source · line 126 · raw

@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> Bool

def is_zero source · line 129 · raw

@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> Bool

def zb source · line 136 · raw

Nat

def mant source · line 140 · raw

@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> Nat

the fraction with the hidden bit 2^52 of a normal number

def xexp source · line 143 · raw

@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> Nat

def rne_up source · line 150 · raw

@+q:Nat -> @+r:Nat -> @+h:Nat -> Nat

m / 2^k rounded to nearest, ties to even: the quotient q, the remainder r and half the divisor h

def rne source · line 153 · raw

@+m:Nat -> @+k:Nat -> Nat

def pack_e source · line 161 · raw

@+s:Bool -> @+ef:Nat -> @+f:Nat -> 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64

a normal number (ef < 2047) or an overflow to infinity

def pack_n source · line 165 · raw

@+s:Bool -> @+q:Nat -> @+u:Nat -> 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64

2^52 <= q < 2^53 is normal with fraction q - 2^52, q < 2^52 subnormal

def pack source · line 171 · raw

@+s:Bool -> @+q:Nat -> @+u:Nat -> 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64

the double nearest to (-1)^s * q * 2^(u - Z) for a q of at most 53 bits at the ulp u (subnormal when q < 2^52), carrying a rounded-up q = 2^53 into 2^52 at the ulp 1 + u

def round_u source · line 176 · raw

@+s:Bool -> @+m:Nat -> @+x:Nat -> @+u:Nat -> 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64

round (-1)^s * m * 2^(x - Z): the ulp is 2^(msb - 52), but never below the subnormal ulp 2^-1074

def round source · line 179 · raw

@+s:Bool -> @+m:Nat -> @+x:Nat -> 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64

def sub_mag source · line 186 · raw

@+sa:Bool -> @+a:Nat -> @+sb:Bool -> @+b:Nat -> @+x:Nat -> @c:Cmp -> 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64

(-1)^sa A + (-1)^sb B at a common scale x: equal magnitudes of opposite signs cancel to +0 (round to nearest)

def add_mag source · line 195 · raw

@+sa:Bool -> @+a:Nat -> @+sb:Bool -> @+b:Nat -> @+x:Nat -> 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64

def add_fin source · line 198 · raw

@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+y:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64

def add_inf source · line 201 · raw

@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+y:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64

def add source · line 204 · raw

@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+y:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64

def neg source · line 208 · raw

@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64

the double with the sign bit flipped (NaN included)

def mul_inf source · line 211 · raw

@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+y:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+s:Bool -> 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64

def mul source · line 214 · raw

@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+y:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64

def kq source · line 218 · raw

Nat

enough quotient bits for any pair of significands, plus a sticky bit

def div_fin source · line 221 · raw

@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+y:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+s:Bool -> 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64

def div_cls source · line 224 · raw

@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+y:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+s:Bool -> 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64

def div source · line 227 · raw

@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+y:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64

def kr source · line 232 · raw

Nat

sqrt(m * 2^(x - Z)) with x - Z made even: the integer square root of the significand scaled by 2^(2 K), and a sticky bit when it was not exact

def sqrt_even source · line 235 · raw

@+m:Nat -> @+x:Nat -> 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64

def sqrt_fin source · line 238 · raw

@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64

def sqrt_cls source · line 241 · raw

@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64

def sqrt source · line 244 · raw

@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64

def mag_cmp source · line 250 · raw

@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+y:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> Cmp

the order of two non-NaN doubles: infinities at the ends, zeros equal

def flip source · line 253 · raw

@c:Cmp -> Cmp

def ord source · line 262 · raw

@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+y:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> Cmp

def ordered source · line 265 · raw

@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+y:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> Bool

def Add.value source · line 270 · raw

@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+y:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> Type

def Sub.value source · line 274 · raw

@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+y:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> Type

x - y is x + (-y)

def Mul.value source · line 277 · raw

@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+y:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> Type

def Div.value source · line 280 · raw

@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+y:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> Type

def Sqrt.value source · line 283 · raw

@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> Type

def Lt.value source · line 286 · raw

@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+y:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> Type

def Le.value source · line 289 · raw

@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+y:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> Type

def Eq.value source · line 292 · raw

@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+y:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> Type

def Neg.value source · line 295 · raw

@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> Type

def Abs.value source · line 298 · raw

@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> Type

def Copysign.value source · line 301 · raw

@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+y:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> Type

def IsNan.value source · line 304 · raw

@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> Type

def IsInf.value source · line 307 · raw

@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> Type

def IsFinite.value source · line 310 · raw

@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> Type

def IsZero.value source · line 313 · raw

@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> Type

def Signbit.value source · line 316 · raw

@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> Type

def OfNat.value source · line 320 · raw

@+n:Nat -> Type

exact below 2^53, rounded above (the runtime bounds Nat by 2^48)

def integral source · line 329 · raw

@m:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.RMode -> @+s:Bool -> @+n:Nat -> @+k:Nat -> Nat

the integer magnitude of (-1)^s * m * 2^-k, k >= 1, in each direction: the integer part high(k, m), plus one when the discarded low(k, m) is nonzero and the direction is away from zero (floor of a negative, ceil of a positive), or to nearest with ties to even (rne)

def to_integral source · line 343 · raw

@m:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.RMode -> @+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64

NaN gives NaN, an infinity or a value of at least 2^52 is already integral, anything else is its integer (with the sign of x, so -0.5 goes to -0 under trunc, ceil and round)

def Trunc.value source · line 346 · raw

@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> Type

def Floor.value source · line 349 · raw

@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> Type

def Ceil.value source · line 352 · raw

@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> Type

def Round.value source · line 355 · raw

@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> Type

def int_part source · line 361 · raw

@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> Nat

the integer part of |x| (x finite)

def to_nat source · line 367 · raw

@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+w:Nat -> Result<&2, &2, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.NumError, Nat>

x truncated toward zero as a w-bit unsigned integer: NaN is a domain error; an infinity, a truncation below zero or one of 2^w or more an overflow (3.1: int(x) truncates; 2.6: fixed widths raise instead of wrapping)

def rv64 source · line 370 · raw

@r:Result<&2, &2, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.NumError, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64> -> Result<&2, &2, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.NumError, Nat>

def rv32 source · line 377 · raw

@r:Result<&2, &2, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.NumError, U32> -> Result<&2, &2, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.NumError, Nat>

def ToU64.value source · line 384 · raw

@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> Type

def ToU32.value source · line 387 · raw

@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> Type

def FloorU64.value source · line 390 · raw

@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> Type

def CeilU64.value source · line 393 · raw

@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> Type

def RoundU64.value source · line 396 · raw

@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> Type

def OfU64.value source · line 400 · raw

@+w:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> Type

the double nearest to an unsigned integer (exact below 2^53)

def OfU32.value source · line 403 · raw

@+u:U32 -> Type

def exp_of source · line 409 · raw

@+t:Nat -> 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Exp

t - Z as a signed exponent

def frexp source · line 415 · raw

@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> Pair(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Exp)

(m, e) with x = m 2^e and 1/2 <= |m| < 1: m is mant(x) scaled by 2^-bit_length(mant(x)) (exact), e the rest of the scale; NaN gives (NaN, 0), zeros and infinities (x, 0) (4.4)

def Frexp.value source · line 418 · raw

@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> Type

def ldexp source · line 424 · raw

@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+neg:Bool -> @+k:Nat -> 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64

x 2^e rounded once: overflow to infinity, gradual underflow (4.4); a scale below 2^-Z is a product under 2^-2947, which rounds to a zero like the scale 0 it is cut to

def Ldexp.value source · line 427 · raw

@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+neg:Bool -> @+k:Nat -> Type

def Ulp.value source · line 432 · raw

@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> Type

the weight of the last bit of x: 2^(xexp(x) - Z) (the smallest subnormal for zeros), inf for infinities, NaN for NaN (4.4)

def pat source · line 438 · raw

@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> Nat

the magnitude bits: exponent field and fraction as one integer below 2^63

def of_pat source · line 441 · raw

@+s:Bool -> @+p:Nat -> 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64

def nextafter source · line 449 · raw

@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+y:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64

the ordered-set neighbour (IEEE nextAfter, C99 annex F): NaN in, NaN out; y when x == y; from a zero the smallest subnormal with y's sign; otherwise one step of the magnitude bits, up when moving away from zero (the step past the largest finite double is infinity, the step below the smallest subnormal a zero of x's sign)

def Nextafter.value source · line 452 · raw

@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+y:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> Type

def fmin source · line 457 · raw

@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+y:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64

IEEE 754-2019 minimumNumber / maximumNumber (10: fmin/fmax fix the order dependence of min/max with NaN): a NaN operand is ignored, -0 < +0

def fmax source · line 460 · raw

@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+y:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64

def Fmin.value source · line 463 · raw

@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+y:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> Type

def Fmax.value source · line 466 · raw

@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+y:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> Type

def IsNormal.value source · line 471 · raw

@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> Type

def IsSubnormal.value source · line 474 · raw

@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> Type

def Bits.value source · line 478 · raw

@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> Type

the 64-bit pattern: sign, exponent field, fraction

def Bits.roundtrip source · line 481 · raw

@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> Type

def Bits.inverse source · line 484 · raw

@+w:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> Type

def IsInteger.value source · line 488 · raw

@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> Type

finite with no fractional bits

def modf source · line 495 · raw

@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> Pair(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64)

(fractional part, integral part), both with the sign of x, both exact: modf(-2.0) = (-0.0, -2.0), modf(inf) = (0.0, inf) (4.3)

def Modf.value source · line 498 · raw

@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> Type

def rsc source · line 502 · raw

@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+y:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> Nat

the significands of x and y at their common scale

def ra source · line 505 · raw

@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+y:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> Nat

def rb source · line 508 · raw

@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+y:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> Nat

def rbad source · line 511 · raw

@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+y:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> Bool

def fmod source · line 517 · raw

@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+y:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64

x - n y with n = trunc(x / y): the exact remainder of the scaled significands, with the sign of x; NaN for NaN, an infinite x or a zero y; x for an infinite y (4.3: fmod(x, inf) == x)

def Fmod.value source · line 520 · raw

@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+y:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> Type

def rflip source · line 527 · raw

@+r:Nat -> @+b:Nat -> @+q:Nat -> Bool

IEEE remainder, x - n y with n = x / y rounded to nearest, ties to even: from r = A mod B and q = A div B, n is q + 1 when r is past half of B (or exactly half with q odd), which leaves B - r with the opposite sign; a zero result has the sign of x (4.3)

def rnear source · line 530 · raw

@+s:Bool -> @+r:Nat -> @+b:Nat -> @+q:Nat -> @+u:Nat -> 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64

def remainder source · line 533 · raw

@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+y:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64

def Remainder.value source · line 536 · raw

@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+y:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> Type

def lt_s source · line 541 · raw

@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+y:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> Bool

def le_s source · line 544 · raw

@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+y:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> Bool

def eq_s source · line 547 · raw

@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+y:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> Bool

def fabs source · line 550 · raw

@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64

def ic_near source · line 556 · raw

@+a:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+b:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+rel:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+at:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+d:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> Bool

CPython's math.isclose, computed in binary64: a negative tolerance is a domain error; a == b is close, an infinity is close only to itself, and otherwise |b - a| <= max(|rel * b|, |rel * a|, abs_tol) (4.4)

def isclose source · line 559 · raw

@+a:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+b:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+rel:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+at:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> Result<&2, &2, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.NumError, Bool>

def IsClose.value source · line 562 · raw

@+a:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+b:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+rel:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+at:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> Type

def tz source · line 566 · raw

@fuel:Nat -> @+n:Nat -> Nat

trailing zero bits of n (at most fuel)

def rtriple source · line 577 · raw

@r:Result<&2, &2, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.NumError, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Ratio> -> Result<&2, &2, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.NumError, Rat>

def as_ratio source · line 588 · raw

@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> Result<&2, &2, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/num.NumError, Rat>

x = +-num / 2^den in lowest terms: the significand with as many of its trailing zeros moved into the denominator as the scale allows; a zero is 0/1 (Python's ints have no -0); NaN is a domain error, an infinity or an integer of 2^64 or more an overflow (3.3)

def AsIntegerRatio.value source · line 591 · raw

@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> Type