def capacity_complete

bendtorch-core@0.1.0.0 · src/shape/construct_proofs.bend:56

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

56def capacity_complete(+dims: List<&2, Nat>, +bound: Shape.LE(Shape.numel(dims), 1048576n)) -> {True{} == within(dims, Shape.capacity(dims)) : Bool}:
57  match dims:
58    case Nil{}:
59      {==}
60    case +head <> +tail:
61      match head:
62        case 0n:
63          zero_within(tail, Shape.capacity(tail))
64        case 1n+p:
65          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)