def Flat.depth.go

bend-tensors@0.0.0.2 · bend_tensors.bend:1687

import Base

1687# the smallest d with 2^d >= n; the fuel bounds the doubling steps
1688def Flat.depth.go(fuel: Nat, +d: Nat, +cap: Nat, +n: Nat, lt: Bool) -> Nat:
1689  match fuel lt:
1690    case _ False{}:
1691      d
1692    case 0n _:
1693      d
1694    case 1n+f True{}:
1695      +cap2 = Nat.add(cap, cap)
1696      Flat.depth.go(f, 1n+d, cap2, n, Nat.is_lt(cap2, n))