law slice_step_refused

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

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

195law slice_step_refused:
196  for +input: Shape.Shape
197  for +dim: U32
198  for +start: U32
199  for +stop: U32
200  for +step: U32
201  for inside: {Nat.is_lt(U32.to_nat(dim), Shape.rank_dimensions(Shape.dimensions(input))) == True{} : Bool}
202  for zero: {U32.to_nat(step) == 0n : Nat}
203  {Slice.plan(input, dim, start, stop, step) == Fail{Slice.StepNotPositive{}} : Result<&2, &2, Slice.Error, Slice.Planned>}