def inside_count

bendtorch-core@0.1.0.0 · src/autograd/reduce_replayed_proof.bend:1036

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

1036def inside_count(+target: Shape.Shape, +index: U32,
1037  +inside: {Nat.is_lt(U32.to_nat(index), Shape.logical_numel(Shape.dimensions(target))) == True{} : Bool}) ->
1038  {Nat.is_lt(U32.to_nat(index), U32.to_nat(Shape.count(target))) == True{} : Bool}:
1039  %Equal.sym(Nat, U32.to_nat(Shape.count(target)), Shape.logical_numel(Shape.dimensions(target)), Reads.count_exact(target)) :
1040    {Nat.is_lt(U32.to_nat(index), _) == True{} : Bool}
1041  inside