def rne_c

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

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

64def rne_c(+q: Nat, +c: Cmp) -> Nat:
65  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)))))