law construction_complete

bendtorch-core@0.1.0.0 · src/shape/LAWS.bend:160

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

160law construction_complete:
161  for +input: List<&2, U32>
162  for rank_bound: Shape.LE(Shape.rank_dimensions(input), 4n)
163  for capacity_bound: Shape.LE(Shape.logical_numel(input), 1048576n)
164  {built(input, Shape.construct(input)) == Some{input} : Maybe<&2, List<&2, U32>>}