def rne
import bend-collections-laws-math@1.0.0.0/spec/math/f64.bend as F64import Base
import bend-collections-laws-math@1.0.0.0/spec/lib/common.bend as C
153def rne(+m: Nat, +k: Nat) -> Nat:
154 match k:
155 case 0n:
156 m
157 case 1n+ +j:
158 rne_up(C.high(1n+j, m), C.low(1n+j, m), C.shift(j, 1n))
Uses (5)
Used by (37)
- bend-collections-laws-math@1.0.0.0/spec/math/f64:round_u
- bend-collections-laws-math@1.0.0.0/spec/math/f64:integral
- 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/f64addc:r1926
- bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64exp:ru
- …