def rflip

bend-collections-laws-crypto@1.0.0.0 · spec/math/f64.bend:523

import Base

523# IEEE remainder, x - n y with n = x / y rounded to nearest, ties to even:
524# from r = A mod B and q = A div B, n is q + 1 when r is past half of B (or
525# exactly half with q odd), which leaves B - r with the opposite sign; a zero
526# result has the sign of x (4.3)
527def rflip(+r: Nat, +b: Nat, +q: Nat) -> Bool:
528  Bool.or(Nat.is_lt(b, Nat.add(r, r)), Bool.and(Nat.is_eq(Nat.add(r, r), b), Nat.is_eq(Nat.mod(q, 2n), 1n)))