def to_u64_value

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

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/num.bend as NE
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64tools.bend as T

189def to_u64_value(+x: F.F64) -> SF.ToU64.value(x):
190  +e1 = Equal.cong(Nat, Result<&2, &2, NE.NumError, Nat>, u => SF.rv64(F.tu_cls(x, Nat.is_eq(u, 2047n))), F.exp_field(x), SF.efield(x), T.ea(x))
191  Equal.trans(Result<&2, &2, NE.NumError, Nat>, SF.rv64(F.to_u64(x)), SF.rv64(F.tu_cls(x, Nat.is_eq(SF.efield(x), 2047n))), SF.to_nat(x, 64n), e1, tu_c(x, Nat.is_eq(SF.efield(x), 2047n), Nat.is_eq(SF.frac(x), 0n), T.fz(x)))