Bitset.depth_go: def of bend-collections@1.0.0.0
Import: import bend-collections@1.0.0.0/src/containers/bitset.bend as Bitset
Lines 152-163 of bend-collections@1.0.0.0/src/containers/bitset.bend: https://jend.leeeet.dev/read.txt?path=bend-collections@1.0.0.0/src/containers/bitset.bend&start_line=152&end_line=163

import Base

# The smallest depth whose 2^depth words hold n bits, capped at max_depth.
# `fuel` bounds the search structurally, `cap` is 2^d and `done` is the exit
# test `n <= 32 * cap`, so a depth that comes out of the loop below the cap
# always satisfies it (proofs/bitset/depth.bend).
def depth_go(fuel: Nat, +n: Nat, d: Nat, +cap: Nat, done: Bool) -> Nat:
  match fuel done:
    case 0n _:
      d
    case 1n+f True{}:
      d
    case 1n+f False{}:
      depth_go(f, n, 1n+d, Nat.double(cap), Nat.is_le(n, Nat.mul(Nat.double(cap), 32n)))

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=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.double
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_le
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.mul