law slice_start_kept

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

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

28# PyTorch's clamp of a slice to an axis of extent n. A start at most n is
29# kept, a start past n becomes n.
30law slice_start_kept:
31  for +extent: Nat
32  for +start: Nat
33  for +stop: Nat
34  for inside: {Nat.is_le(start, extent) == True{} : Bool}
35  {low(Slice.bounds(extent, start, stop)) == start : Nat}