law narrow_rest

bendtorch@1.3.0.0 · LAWS.bend:277

import Base
import bendtorch@1.3.0.0/tensor.bend as TT

277# LAW (narrow_rest): narrow (and setting any axis' size) changes only its own axis: with axis d taken out, the shape is
278# what it was.
279law narrow_rest:
280  for +s: List<&2, Nat>
281  for +d: Nat
282  for +l: Nat
283  {TT.remove(TT.setd(s, d, l), d) == TT.remove(s, d) : List<&2, Nat>}