law slice_stop_kept

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

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

44# A stop from the start to n is kept, a stop past n becomes n, and a stop
45# at or before the start ends the slice at its start: an empty axis.
46law slice_stop_kept:
47  for +extent: Nat
48  for +start: Nat
49  for +stop: Nat
50  for +after: {Nat.is_le(start, stop) == True{} : Bool}
51  for +inside: {Nat.is_le(stop, extent) == True{} : Bool}
52  {high(Slice.bounds(extent, start, stop)) == stop : Nat}