ConstructProofs.capacity_complete: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/shape/construct_proofs.bend as ConstructProofs
Lines 56-65 of bendtorch-core@0.1.0.0/src/shape/construct_proofs.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/shape/construct_proofs.bend&start_line=56&end_line=65

import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/shape/nat_proofs.bend as Nats

def capacity_complete(+dims: List<&2, Nat>, +bound: Shape.LE(Shape.numel(dims), 1048576n)) -> {True{} == within(dims, Shape.capacity(dims)) : Bool}:
  match dims:
    case Nil{}:
      {==}
    case +head <> +tail:
      match head:
        case 0n:
          zero_within(tail, Shape.capacity(tail))
        case 1n+p:
          step_within(p, tail, Shape.capacity(tail), capacity_complete(tail, Nats.le_add_left(Shape.numel(tail), Nat.mul(p, Shape.numel(tail)), 1048576n, bound)), bound)

Uses (11):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.mul
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/construct_proofs.bend&name=step_within
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/construct_proofs.bend&name=within
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/construct_proofs.bend&name=zero_within
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=LE
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=capacity
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=numel
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/nat_proofs.bend&name=le_add_left