def output_inside

bendtorch-core@0.1.0.0 · src/autograd/broadcast_PROOF.bend:124

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

124def output_inside(+plan: Shape.BroadcastPlan, +target: Shape.Shape, +index: U32,
125  -same_dims: {Shape.dimensions(Shape.output_shape(plan)) == Shape.dimensions(target) : List<&2, U32>},
126  -inside: Shape.LT(U32.to_nat(index), Shape.logical_numel(Shape.dimensions(target)))) ->
127  Holds<{Nat.is_lt(U32.to_nat(index), Shape.elements(Shape.output_shape(plan))) == True{} : Bool}>:
128  Holds{
129    %Equal.sym(Nat, Shape.elements(Shape.output_shape(plan)), Shape.numel(Shape.extents(Shape.output_shape(plan))), Shape.elements_exact(Shape.output_shape(plan))) :
130      {Nat.is_lt(U32.to_nat(index), _) == True{} : Bool}
131    %Equal.sym(List<&2, U32>, Shape.dimensions(Shape.output_shape(plan)), Shape.dimensions(target), same_dims) :
132      {Nat.is_lt(U32.to_nat(index), Shape.logical_numel(_)) == True{} : Bool}
133    Equal.sym(Bool, True{}, Nat.is_lt(U32.to_nat(index), Shape.logical_numel(Shape.dimensions(target))),
134      Nats.lt_true(U32.to_nat(index), Shape.logical_numel(Shape.dimensions(target)), inside))}