def mff_c

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

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

70def mff_c(+x: F.F64, +c: Bool) -> {F.mf_fin(x, c) == SF.pickt(F.F64 & F.F64, c, (SF.zero(SF.sign(x)), x), (FRAC(x), SF.to_integral(F.Trunc{}, x))) : F.F64 & F.F64}:
71  match c:
72    case True{}:
73      Equal.cong(F.F64, F.F64 & F.F64, t => (t, x), F.zero(F.signbit(x)), SF.zero(SF.sign(x)), zs(x))
74    case False{}:
75      +A0 = F.mf_frac(F.signbit(x), F.dmant(x), F.dexp(x), Nat.sub(3000n, F.dexp(x)), Nat.is_lt(Nat.sub(3000n, F.dexp(x)), 64n))
76      +p1 = Equal.cong(F.F64, F.F64 & F.F64, t => (t, F.trunc(x)), A0, FRAC(x), frac_v(x))
77      +p2 = Equal.cong(F.F64, F.F64 & F.F64, t => (FRAC(x), t), F.trunc(x), SF.to_integral(F.Trunc{}, x), RI.trunc_value(x))
78      Equal.trans(F.F64 & F.F64, (A0, F.trunc(x)), (FRAC(x), F.trunc(x)), (FRAC(x), SF.to_integral(F.Trunc{}, x)), p1, p2)