law narrow_axis

bendtorch@1.3.0.0 · LAWS.bend:285

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

285# LAW (narrow_axis): narrowing axis d of a tensor that has it gives that axis exactly the length asked for.
286law narrow_axis:
287  for +s: List<&2, Nat>
288  for +d: Nat
289  for +l: Nat
290  for e: {True{} == Nat.is_lt(d, TT.rank(s)) : Bool}
291  {TT.at1(TT.setd(s, d, l), d) == l : Nat}