def rne_up
import bend-collections-laws-math@1.0.0.0/spec/math/f64.bend as F64import Base
148# m / 2^k rounded to nearest, ties to even: the quotient q, the remainder
149# r and half the divisor h
150def rne_up(+q: Nat, +r: Nat, +h: Nat) -> Nat:
151 Nat.add(q, b2n(Bool.or(Nat.is_lt(h, r), Bool.and(Nat.is_eq(r, h), Nat.is_eq(Nat.mod(q, 2n), 1n)))))
Uses (8)
Used by (12)
- bend-collections-laws-math@1.0.0.0/spec/math/f64:rne
- bend-collections-laws-math@1.0.0.0/proofs/math/random/fround:rne_exact
- bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64round:rne_cmp
- bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64round:rp_c
- bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64round:sticky
- …