def modf_value

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64modf.bend:91

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/proofs/math/typed/f64tools.bend as T

91def modf_value(+x: F.F64) -> SF.Modf.value(x):
92  +e1 = Equal.cong(Nat, F.F64 & F.F64, u => F.mf_cls(x, Nat.is_eq(u, 2047n)), F.exp_field(x), SF.efield(x), T.ea(x))
93  Equal.trans(F.F64 & F.F64, F.modf(x), F.mf_cls(x, Nat.is_eq(SF.efield(x), 2047n)), SF.modf(x), e1, mf_c(x, Nat.is_eq(SF.efield(x), 2047n), Nat.is_eq(SF.frac(x), 0n), T.fz(x)))