def upn

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64rint.bend:32

import Base
import bend-collections-laws-math@1.0.0.0/src/math/f64.bend as F

32def upn(+m: F.RMode, +s: Bool, +q: Nat, +r: Nat, +h: Nat) -> Bool:
33  match m:
34    case F.Trunc{}:
35      False{}
36    case F.Floor{}:
37      Bool.and(s, Bool.not(Nat.is_eq(r, 0n)))
38    case F.Ceil{}:
39      Bool.and(Bool.not(s), Bool.not(Nat.is_eq(r, 0n)))
40    case F.Even{}:
41      Bool.or(Nat.is_lt(h, r), Bool.and(Nat.is_eq(r, h), Nat.is_eq(Nat.mod(q, 2n), 1n)))