law signed_last_inside

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

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

31# Last{k} is the position d = -1 - k. In range, it wraps to d + limit:
32# the wrapped position plus k + 1 is limit, in exact arithmetic.
33law signed_last_inside:
34  for +limit: U32
35  for +k: U32
36  for inside: {U32.is_lt(k, limit) == True{} : Bool}
37  {Nat.add(U32.to_nat(Signed.wrap(limit, Signed.Last{k})), 1n+U32.to_nat(k)) == U32.to_nat(limit) : Nat}