def to_u64
import bend-collections-laws-math@1.0.0.0/src/math/f64.bend as F64import Base
import bend-collections-laws-math@1.0.0.0/src/math/num.bend as N
import bend-collections-laws-math@1.0.0.0/src/math/u64.bend as W
784# x truncated toward zero as an unsigned 64-bit integer: NaN is a domain
785# error, a value outside [0, 2^64) (infinities included) an overflow
786def to_u64(+x: F64) -> Result<&2, &2, N.NumError, W.U64>:
787 tu_cls(x, Nat.is_eq(exp_field(x), 2047n))
Uses (7)
Used by (10)
- bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64conv:to_u64_value
- bend-collections-laws-math@1.0.0.0/src/math/f64:to_u32
- bend-collections-laws-math@1.0.0.0/spec/math/f64:ToU64.value
- bend-collections-laws-math@1.0.0.0/src/math/f64:ceil_u64
- bend-collections-laws-math@1.0.0.0/src/math/f64:floor_u64
- …