def to_u32_value

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64conv.bend:248

import Base
import bend-collections-laws-math@1.0.0.0/spec/lib/common.bend as C
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/src/math/num.bend as NE

248def to_u32_value(+x: F.F64) -> SF.ToU32.value(x):
249  +R64 = SF.rv64(F.to_u64(x))
250  +e1 = t32(F.to_u64(x))
251  +e2 = Equal.cong(Result<&2, &2, NE.NumError, Nat>, Result<&2, &2, NE.NumError, Nat>, r => f32r(r), R64, SF.to_nat(x, 64n), to_u64_value(x))
252  +IP = SF.int_part(x)
253  +e3 = s32_c(SF.is_nan(x), SF.is_inf(x), Bool.and(SF.sign(x), Bool.not(Nat.is_eq(IP, 0n))), IP, C.fits(64n, IP), {==})
254  Equal.trans(Result<&2, &2, NE.NumError, Nat>, SF.rv32(F.to_u32(x)), f32r(R64), SF.to_nat(x, 32n), e1, Equal.trans(Result<&2, &2, NE.NumError, Nat>, f32r(R64), f32r(SF.to_nat(x, 64n)), SF.to_nat(x, 32n), e2, e3))