def output_inside
bendtorch-core@0.1.0.0 · src/tensor/permute_values.bend:266
import bendtorch-core@0.1.0.0/src/tensor/permute_values.bend as PermuteValues
import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/tensor/layout.bend as Layout
import bendtorch-core@0.1.0.0/src/tensor/permute_build_proof.bend as PermuteProof
266def output_inside(+input: Shape.Shape, +axes: List<&2, U32>, +plan: Layout.Plan<input, axes>, +index: U32,
267 inside: {Nat.is_lt(U32.to_nat(index), Shape.logical_numel(Shape.dimensions(input))) == True{} : Bool}) ->
268 {Nat.is_lt(U32.to_nat(index), Shape.logical_numel(Shape.dimensions(Layout.output(input, axes, plan)))) == True{} : Bool}:
269 %Equal.sym(Nat, Shape.logical_numel(Shape.dimensions(Layout.output(input, axes, plan))), Shape.logical_numel(Shape.dimensions(input)),
270 PermuteProof.plan_numel(input, axes, plan)) : {Nat.is_lt(U32.to_nat(index), _) == True{} : Bool}
271 inside