ConstructionLAWS.public_construction_complete: law of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/tensor/construction_LAWS.bend as ConstructionLAWS
Lines 85-91 of bendtorch-core@0.1.0.0/src/tensor/construction_LAWS.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/tensor/construction_LAWS.bend&start_line=85&end_line=91

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

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

Uses (13):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=F32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List.length
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/LAWS.bend&name=construction_complete
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=LE
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=construct
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=logical_numel
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=rank_dimensions
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/construction_PROOF.bend&name=construction_shape_complete
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/construction_totality.bend&name=ConstructionDone
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/core.bend&name=construct