def fpk

bend-collections-laws-math@1.0.0.0 · proofs/math/random/fround.bend:231

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

231def fpk(+one: Nat, +h1: {one == 1n : Nat}, +R0: Nat, +hR: {Nat.is_le(R0, C.shift(53n, one)) == True{} : Bool}, +t: Bool) -> {C.fits(53n, SF.pick(Nat, t, Nat.sub(R0, Nat.mod(R0, 2n)), R0)) == C.fits(53n, R0) : Bool}:
232  match t:
233    case True{}:
234      fsub_c(52n, one, h1, R0, hR, C.fits(53n, R0), {==})
235    case False{}:
236      {==}