F64rint.rik: def of bend-collections-laws-math@1.0.0.0
Import: import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64rint.bend as F64rint
Lines 213-218 of bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64rint.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64rint.bend&start_line=213&end_line=218

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

def 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}:
  match k:
    case 0n:
      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)))
    case 1n+ +j:
      rik_c(m, s, w, j, hw, Nat.is_lt(1n+j, 64n), {==})

Uses (16):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Empty.absurd
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_le
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_lt
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64light.bend&name=true_ne_false
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64rint.bend&name=rik_c
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/lib/common.bend&name=fits
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/math/f64.bend&name=integral
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/math/f64.bend&name=round
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/math/w64.bend&name=value
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/f64.bend&name=F64
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/f64.bend&name=RMode
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/f64.bend&name=ri_k
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/u64.bend&name=U64