def ldexp_value

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64exp.bend:254

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

254def ldexp_value(+x: F.F64, +neg: Bool, +k: Nat) -> SF.Ldexp.value(x, neg, k):
255  +e1 = Equal.cong(Nat, F.F64, u => F.ld_cls(x, F.Exp{neg, k}, Nat.is_eq(u, 2047n)), F.exp_field(x), SF.efield(x), T.ea(x))
256  Equal.trans(F.F64, F.ldexp(x, F.Exp{neg, k}), F.ld_cls(x, F.Exp{neg, k}, Nat.is_eq(SF.efield(x), 2047n)), SF.ldexp(x, neg, k), e1, ld_c(x, neg, k, Nat.is_eq(SF.efield(x), 2047n), Nat.is_eq(SF.frac(x), 0n), T.fz(x)))