Fixed.no_prime: def of bend-collections-laws-math@1.0.0.0
Import: import bend-collections-laws-math@1.0.0.0/spec/math/fixed.bend as Fixed
Lines 190-196 of bend-collections-laws-math@1.0.0.0/spec/math/fixed.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-math@1.0.0.0/spec/math/fixed.bend&start_line=190&end_line=196

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

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

Uses (5):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool.and
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool.not
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/math/number.bend&name=prime