def output_bound
bendtorch-core@0.1.0.0 · src/tensor/elementwise_parallel_proof.bend:457
import bendtorch-core@0.1.0.0/src/tensor/elementwise_parallel_proof.bend as ElementwiseParallelProof
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
457def output_bound(+plan: Shape.BroadcastPlan, +index: U32, +bound: Shape.LT(U32.to_nat(index), Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan))))) ->
458 {True{} == Nat.is_lt(U32.to_nat(index), Shape.elements(Shape.output_shape(plan))) : Bool}:
459 %Equal.sym(Nat, Shape.elements(Shape.output_shape(plan)), Shape.numel(Shape.extents(Shape.output_shape(plan))), Shape.elements_exact(Shape.output_shape(plan))) :
460 {True{} == Nat.is_lt(U32.to_nat(index), _) : Bool}
461 Nats.lt_true(U32.to_nat(index), Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan))), bound)