law slice_length_below

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

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

68# The length of the sliced axis is the number of indices start, start +
69# step, start + 2 step, ... below the stop: each index below the length
70# lies below the stop, and, for a positive step, the index at the length
71# does not.
72law slice_length_below:
73  for +start: Nat
74  for +stop: Nat
75  for +step: Nat
76  for +k: Nat
77  for below: {Nat.is_lt(k, Slice.length(Slice.Bounds{start, stop}, step)) == True{} : Bool}
78  {Nat.is_lt(Nat.add(start, Nat.mul(k, step)), stop) == True{} : Bool}