def ulp_value

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64misc.bend:47

import Base
import bend-collections-laws-math@1.0.0.0/spec/math/f64.bend as SF
import bend-collections-laws-math@1.0.0.0/src/math/f64.bend as F
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64tools.bend as T

47def ulp_value(+x: F.F64) -> SF.Ulp.value(x):
48  +e1 = Equal.cong(Nat, F.F64, t => F.ulp_cls(x, Nat.is_eq(t, 2047n)), F.exp_field(x), SF.efield(x), T.ea(x))
49  Equal.trans(F.F64, F.ulp(x), F.ulp_cls(x, Nat.is_eq(SF.efield(x), 2047n)), SF.pick(F.F64, SF.is_nan(x), SF.qnan(), SF.pick(F.F64, SF.is_inf(x), SF.inf(False{}), SF.round(False{}, 1n, SF.xexp(x)))), e1, ulp_c(x, Nat.is_eq(SF.efield(x), 2047n), Nat.is_eq(SF.frac(x), 0n), T.fz(x)))