def pko

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64round.bend:547

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

547def pko(+s: Bool, +q: Nat, +u: Nat, +EF: Nat, +hEF: {Nat.add(EF, 1926n) == u : Nat}, +h52: {C.fits(52n, q) == False{} : Bool}, +hov: {Nat.is_lt(Nat.add(EF, SF.pick(Nat, C.fits(53n, q), 1n, 2n)), 2047n) == False{} : Bool}) -> {SF.pack(s, q, u) == SF.inf(s) : F.F64}:
548  pko_c(s, q, u, EF, hEF, C.fits(53n, q), h52, hov)