def of_u32_value

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

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/src/math/u64.bend as WU
import bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend as N
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64tools.bend as T

29def of_u32_value(+u: U32) -> SF.OfU32.value(u):
30  +e1 = T.rw_value(False{}, 3000n, WU.U64{u, 0}, {==})
31  +e2 = Equal.cong(Nat, F.F64, t => SF.round(False{}, t, 3000n), Nat.add(v(u), 0n), v(u), N.add_zero(v(u)))
32  Equal.trans(F.F64, F.of_u32(u), SF.round(False{}, Nat.add(v(u), 0n), 3000n), SF.round(False{}, v(u), SF.zb()), e1, e2)