def rp_c2

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64round.bend:910

import Base
import bend-collections-laws-math@1.0.0.0/spec/lib/common.bend as C
import bend-collections-laws-math@1.0.0.0/spec/math/f64.bend as SF
import bend-collections-laws-math@1.0.0.0/spec/math/w64.bend as SW
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/u64.bend as WU

910def rp_c2(+one: Nat, +h1: {one == 1n : Nat}, +s: Bool, +e: Nat, +sig: WU.U64, +x: Nat, +hx: {Nat.add(x, 2180n) == e : Nat}, +h62: {C.fits(62n, SW.value(sig)) == False{} : Bool}, +h63: {C.fits(63n, SW.value(sig)) == True{} : Bool}, +b: Bool, +hb: {Nat.is_lt(x, 1916n) == b : Bool}, +u: Nat, +hu: {Nat.max(Nat.add(10n, x), 1926n) == u : Nat}) -> {F.rp_neg(s, e, sig, b) == SF.round_u(s, SW.value(sig), x, u) : F.F64}:
911  match b:
912    case True{}:
913      rp_sub(one, h1, s, e, sig, x, hx, h62, h63, hb, u, hu)
914    case False{}:
915      rp_norm(one, h1, s, e, sig, x, hx, h62, h63, hb, u, hu)