~/bend-docscommunity

proofs/math/typed/f64misc.bend checks

raw source on the hub · import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64misc.bend as F64misc

12 imports
import Base
import ../../../spec/lib/common.bend as C
import ../../../spec/math/f64.bend as SF
import ../../../src/math/f64.bend as F
import ../../../src/math/w64.bend as X
import ../../../src/math/u64.bend as WU
import ../../lib/nat.bend as N
import ../../lib/lemmas/proofs/nat_algebra.bend as NA
import ./width.bend as WW
import ./f64bits.bend as FB
import ./f64cmp.bend as FC
import ./f64tools.bend as T

Definitions

def v source · line 21 · raw

@+x:U32 -> Nat

def of_u64_value source · line 26 · raw

@+w:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.OfU64.value(w)

def of_u32_value source · line 29 · raw

@+u:U32 -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.OfU32.value(u)

def ulp_c source · line 36 · raw

@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+t:Bool -> @+z:Bool -> @+hz:{0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.is_zero(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.frac(x)) == z : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.ulp_cls(x, t) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.pick(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64, Bool.and(t, Bool.not(z)), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.qnan, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.pick(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64, Bool.and(t, z), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.inf(False{}), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.round(False{}, 1n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.xexp(x)))) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}

def ulp_value source · line 47 · raw

@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.Ulp.value(x)

def is_normal_value source · line 53 · raw

@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.IsNormal.value(x)

def is_subnormal_value source · line 56 · raw

@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.IsSubnormal.value(x)

def bits_g source · line 63 · raw

@+l:U32 -> @+h:U32 -> {Nat.add(v(l), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(32n, v(h))) == Nat.add(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.pat(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{l, h}), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/lib/common.shift(63n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.b2n(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.sign(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{l, h})))) : Nat}

def bits_value source · line 81 · raw

@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.Bits.value(x)

def bits_roundtrip source · line 86 · raw

@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.Bits.roundtrip(x)

def bits_inverse source · line 91 · raw

@+w:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.Bits.inverse(w)