def rne_norm

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

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

457# a normalized m (bit 62 set) rounds to a normal significand
458def rne_norm(+m: Nat, +hm: {C.fits(62n, m) == False{} : Bool}) -> {C.fits(52n, SF.rne(m, 10n)) == False{} : Bool}:
459  +f = Equal.trans(Bool, C.fits(52n, C.high(10n, m)), C.fits(62n, m), False{}, Equal.sym(Bool, C.fits(62n, m), C.fits(52n, C.high(10n, m)), fits_hc(10n, 52n, m)), hm)
460  nfit(52n, C.high(10n, m), SF.rne(m, 10n), rne_lb(m), f)