def no_prime

bend-collections-laws-math@1.0.0.0 · spec/math/fixed.bend:190

import Base
import bend-collections-laws-math@1.0.0.0/spec/math/number.bend as SN

190# no prime m with lo <= m < lo + k
191def no_prime(k: Nat, +lo: Nat) -> Bool:
192  match k:
193    case 0n:
194      True{}
195    case 1n+p:
196      Bool.and(Bool.not(SN.prime(lo)), no_prime(p, 1n+lo))