law slice_view_around

bendtorch-core@0.1.0.0 · src/tensor/slice_LAWS.bend:87

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

87# The row-major view around axis `dim` of dimensions prefix ++ [extent] ++
88# suffix, with `dim` the rank of the prefix: the element count of the
89# prefix, the extent, and the element count of the suffix.
90law slice_view_around:
91  for +prefix: List<&2, U32>
92  for +extent: U32
93  for +suffix: List<&2, U32>
94  {Slice.view(List.append(&2, U32, prefix, extent <> suffix), Shape.rank_dimensions(prefix)) ==
95    Slice.View{Shape.logical_numel(prefix), U32.to_nat(extent), Shape.logical_numel(suffix)} : Slice.View}