Number.prime_go: def of bend-collections-laws-math@1.0.0.0
Import: import bend-collections-laws-math@1.0.0.0/src/math/number.bend as Number
Lines 63-74 of bend-collections-laws-math@1.0.0.0/src/math/number.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-math@1.0.0.0/src/math/number.bend&start_line=63&end_line=74

import Base

# trial division: no d in [2, n) divides n iff none in [2, isqrt(n)] does.
# `done` is n < d*d, `divides` is d | n, both for the current d.
def prime_go(fuel: Nat, +n: Nat, +d: Nat, done: Bool, divides: Bool) -> Bool:
  match fuel done divides:
    case 0n _ _:
      True{}
    case 1n+f True{} _:
      True{}
    case 1n+f False{} True{}:
      False{}
    case 1n+ +f False{} False{}:
      prime_go(f, n, 1n+d, Nat.is_lt(n, Nat.mul(1n+d, 1n+d)), Nat.is_eq(Nat.mod(n, 1n+d), 0n))

Uses (6):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_eq
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_lt
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.mod
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.mul