law signed_capped_classifies

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

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

269# The inference never forms the exact sizes' product: capped classifies it
270# against the input's element count, ZeroProduct, Within{p} with p at most
271# the count, or Beyond, multiplying only numbers at most the count. So the
272# inferred size is worked out from numbers at most 2^20, however large the
273# exact sizes, as [-1, 2^24, 2^24] of an empty input, whose product 2^48 is
274# past the native Nat limit.
275law signed_capped_classifies:
276  for +bound: Nat
277  for +extents: List<&2, Signed.Extent>
278  {Signed.capped(bound, extents) == classify(bound, Signed.exact_product(extents)) : Signed.Product}