def round_u64_value

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

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/f64rint.bend as RI

264def round_u64_value(+x: F.F64) -> SF.RoundU64.value(x):
265  Equal.trans(Result<&2, &2, NE.NumError, Nat>, SF.rv64(F.to_u64(F.round(x))), SF.to_nat(F.round(x), 64n), SF.to_nat(SF.to_integral(F.Even{}, x), 64n), to_u64_value(F.round(x)), Equal.cong(F.F64, Result<&2, &2, NE.NumError, Nat>, y => SF.to_nat(y, 64n), F.round(x), SF.to_integral(F.Even{}, x), RI.round_value(x)))