BendMlTensorFork.depth_go: def of bend-ml-tensor-fork@0.1.6.0
Import: import bend-ml-tensor-fork@0.1.6.0/main.bend as BendMlTensorFork
Lines 113-122 of bend-ml-tensor-fork@0.1.6.0/main.bend: https://jend.leeeet.dev/read.txt?path=bend-ml-tensor-fork@0.1.6.0/main.bend&start_line=113&end_line=122

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

# the smallest d with 2^d >= n (TA.cap_depth's answer) by doubling a U32: log2(n) steps, where cap_depth compares Nats
# (a share of every product's time at 512 x 1536)
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