law public_construction_complete

bendtorch-core@0.1.0.0 · src/tensor/construction_LAWS.bend:85

import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/tensor/core.bend as Core
import bendtorch-core@0.1.0.0/src/tensor/construction_totality.bend as Totality

85law public_construction_complete:
86  for +dimensions: List<&2, U32>
87  for +values: List<&2, F32>
88  for rank_bound: Shape.LE(Shape.rank_dimensions(dimensions), 4n)
89  for capacity_bound: Shape.LE(Shape.logical_numel(dimensions), 1048576n)
90  for counted: {List.length(&2, F32, values) == Shape.logical_numel(dimensions) : Nat}
91  Totality.ConstructionDone<dimensions, Core.construct(dimensions, values)>