law signed_narrow_before

bendtorch-core@0.1.0.0 · src/tensor/signed_LAWS.bend:392

import Base
import bendtorch-core@0.1.0.0/src/tensor/core.bend as Core
import bendtorch-core@0.1.0.0/src/tensor/signed.bend as Signed
import bendtorch-core@0.1.0.0/src/tensor/slice.bend as Slice

392# ... and a start before -extent is refused: OutOfRange once the axis is in
393# range, and AxisOutOfBounds first, as the unsigned narrow checks it.
394law signed_narrow_before:
395  for input: Core.Dynamic
396  for +dim: Signed.Position
397  for +k: U32
398  for +length: U32
399  for in_rank: {Nat.is_lt(U32.to_nat(axis_of(input, dim)), rank_of(input)) == True{} : Bool}
400  for before: {U32.is_lt(k, extent_of(input, axis_of(input, dim))) == False{} : Bool}
401  {Signed.narrow(input, dim, Signed.Last{k}, length) == (input, Fail{Slice.OutOfRange{}}) :
402    Core.Dynamic & Result<&2, &1, Slice.Error, Core.Dynamic>}