def rik

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

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/spec/math/w64.bend as SW
import bend-collections-laws-math@1.0.0.0/src/math/f64.bend as F
import bend-collections-laws-math@1.0.0.0/src/math/u64.bend as WU
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64light.bend as FL

213def rik(+m: F.RMode, +s: Bool, +w: WU.U64, +k: Nat, +hk: {Nat.is_le(1n, k) == True{} : Bool}, +hw: {C.fits(53n, SW.value(w)) == True{} : Bool}) -> {F.ri_k(m, s, w, k, Nat.is_lt(k, 64n)) == SF.round(s, SF.integral(m, s, SW.value(w), k), 3000n) : F.F64}:
214  match k:
215    case 0n:
216      Empty.absurd({F.ri_k(m, s, w, 0n, Nat.is_lt(0n, 64n)) == SF.round(s, SF.integral(m, s, SW.value(w), 0n), 3000n) : F.F64}, FL.true_ne_false(Equal.sym(Bool, False{}, True{}, hk)))
217    case 1n+ +j:
218      rik_c(m, s, w, j, hw, Nat.is_lt(1n+j, 64n), {==})