def pack_v

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64round.bend:377

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/spec/math/w64.bend as SW
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/w64.bend as X
import bend-collections-laws-math@1.0.0.0/src/math/u64.bend as WU

377def pack_v(+s: Bool, +e: Nat, +he: {C.fits(11n, e) == True{} : Bool}, +m: WU.U64, +hn: {C.fits(63n, Nat.add(SW.value(m), C.shift(52n, e))) == True{} : Bool}) -> {F.pack(s, e, m) == bits(s, Nat.add(SW.value(m), C.shift(52n, e))) : F.F64}:
378  +e0 = Equal.cong(U32, F.F64, z => F.pack64(X.add(WU.U64{0, U32.add(z, U32.mul(U32.from_nat(e), 1048576))}, m)), F.sgn(s), SF.pick(U32, s, 2147483648, 0), sgn_pick(s))
379  Equal.trans(F.F64, F.pack(s, e, m), F.pack64(X.add(WU.U64{0, U32.add(SF.pick(U32, s, 2147483648, 0), U32.mul(U32.from_nat(e), 1048576))}, m)), bits(s, Nat.add(SW.value(m), C.shift(52n, e))), e0, pack_g(1n, {==}, s, e, he, m, hn, 2147483648, {==}, 1048576, {==}))