def round_shift

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

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

150# round(s, m * 2^k, x) = round(s, m, x + k)
151def round_shift(+s: Bool, +k: Nat, +m: Nat, +x: Nat) -> {SF.round(s, C.shift(k, m), x) == SF.round(s, m, Nat.add(x, k)) : F.F64}:
152  rs_c(s, k, m, x, Nat.is_eq(m, 0n), {==})