def output_inside

bendtorch-core@0.1.0.0 · src/tensor/contracts/broadcast_proof.bend:16

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

16def output_inside(+plan: Shape.BroadcastPlan, +index: Nat,
17  below: {Nat.is_lt(index, Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan)))) == True{} : Bool}) ->
18  {True{} == Nat.is_lt(index, Shape.elements(Shape.output_shape(plan))) : Bool}:
19  %Equal.sym(Nat, Shape.elements(Shape.output_shape(plan)), Shape.numel(Shape.extents(Shape.output_shape(plan))),
20    Shape.elements_exact(Shape.output_shape(plan))) : {True{} == Nat.is_lt(index, _) : Bool}
21  Equal.sym(Bool, Nat.is_lt(index, Shape.logical_numel(Shape.dimensions(Shape.output_shape(plan)))), True{}, below)