def rud

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64rtools.bend:131

import Base
import bend-collections-laws-math@1.0.0.0/spec/lib/common.bend as C
import bend-collections-laws-math@1.0.0.0/spec/math/f64.bend as SF
import bend-collections-laws-math@1.0.0.0/src/math/f64.bend as F

131def rud(+s: Bool, +m: Nat, +x: Nat, +u: Nat) -> {SF.round_u(s, m, x, u) == SF.pack(s, SF.pick(Nat, Nat.is_le(x, u), SF.rne(m, Nat.sub(u, x)), C.shift(Nat.sub(x, u), m)), u) : F.F64}:
132  {==}