law signed_filled_count

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

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

215# And then the filled sizes hold q * p elements.
216law signed_filled_count:
217  for +extents: List<&2, Signed.Extent>
218  for one: {Signed.inferred_count(extents) == 1n : Nat}
219  for +size: U32
220  {Shape.logical_numel(Signed.filled(extents, size)) == Nat.mul(U32.to_nat(size), Signed.exact_product(extents)) : Nat}