def nfit

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

import Base
import bend-collections-laws-math@1.0.0.0/spec/lib/common.bend as C

454def nfit(+k: Nat, +a: Nat, +r: Nat, +hle: {Nat.is_le(a, r) == True{} : Bool}, +f: {C.fits(k, a) == False{} : Bool}) -> {C.fits(k, r) == False{} : Bool}:
455  nfit_c(k, a, r, hle, f, C.fits(k, r), {==})