law cat_numel

bendtorch@1.3.0.0 · LAWS.bend:293

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

293# LAW (cat_numel): concatenating along an axis the tensor has adds the counts: a tensor whose axis d is x + y long holds
294# as many numbers as the two with x and y.
295law cat_numel:
296  for +s: List<&2, Nat>
297  for +d: Nat
298  for +x: Nat
299  for +y: Nat
300  for e: {True{} == Nat.is_lt(d, TT.rank(s)) : Bool}
301  {TT.numel(TT.setd(s, d, Nat.add(x, y))) == Nat.add(TT.numel(TT.setd(s, d, x)), TT.numel(TT.setd(s, d, y))) : Nat}