Bendtorch.depth_go: def of bendtorch@1.3.0.0
Import: import bendtorch@1.3.0.0/main.bend as Bendtorch
Lines 211-220 of bendtorch@1.3.0.0/main.bend: https://jend.leeeet.dev/read.txt?path=bendtorch@1.3.0.0/main.bend&start_line=211&end_line=220

import Base
import bend-ml-tensor-array@0.1.18.0/main.bend as TA

# the smallest d with 2^d >= n (TA.cap_depth's answer), by doubling a U32: log2(n) cheap steps, where cap_depth
# compares Nats one unit at a time at each doubling; f is fuel (32 doublings cover every U32)
def depth_go(f: Nat, ok: Bool, +n: U32, +p: U32, d: Nat) -> Nat:
  match f ok:
    case _ True{}:
      d
    case 0n False{}:
      d
    case 1n+g False{}:
      depth_go(g, U32.is_le(n, (p + p : U32)), n, (p + p : U32), 1n+d)

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