def rne_c

bend-collections-laws-math@1.0.0.0 · proofs/math/random/fround.bend:44

import Base
import bend-collections-laws-math@1.0.0.0/spec/math/f64.bend as SF

44def rne_c(+q: Nat, +c: Cmp) -> Nat:
45  Nat.add(q, SF.b2n(Bool.or(Cmp.is_lt(SF.flip(c)), Bool.and(Cmp.is_eq(c), Nat.is_eq(Nat.mod(q, 2n), 1n)))))