~/jendhub

def nfit

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

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

148def 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}:
149  nfit_c(k, a, r, hle, f, C.fits(k, r), {==})

Uses (5)

Used by (1)