def construction_shape_complete
bendtorch-core@0.1.0.0 · src/tensor/construction_PROOF.bend:689
import bendtorch-core@0.1.0.0/src/tensor/construction_PROOF.bend as ConstructionPROOF
import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/storage/arith.bend as Arith
import bendtorch-core@0.1.0.0/src/tensor/core.bend as Core
import bendtorch-core@0.1.0.0/src/shape/LAWS.bend as ShapeLaws
import bendtorch-core@0.1.0.0/src/tensor/construction_totality.bend as Totality
689def construction_shape_complete(+dimensions: List<&2, U32>, +values: List<&2, F32>, result: Shape.ConstructResult<dimensions>,
690 built: {ShapeLaws.built(dimensions, result) == Some{dimensions} : Maybe<&2, List<&2, U32>>},
691 +counted: {List.length(&2, F32, values) == Shape.logical_numel(dimensions) : Nat}) ->
692 Totality.ConstructionDone<dimensions, Core.construct_shape(dimensions, values, result)>:
693 match result:
694 case Shape.SError{error}:
695 Totality.ConstructionDone{
696 Empty.absurd(Totality.ConstructionWitness<dimensions, Fail{Core.ShapeError{error}}>,
697 Arith.clash(Equal.cong(Maybe<&2, List<&2, U32>>, Bool, Maybe.is_some(&2, List<&2, U32>), None{}, Some{dimensions}, built))),
698 Equal.cong(Maybe<&2, List<&2, U32>>, Bool, Maybe.is_some(&2, List<&2, U32>), None{}, Some{dimensions}, built), Unit{}}
699 case Shape.SBuilt{+shape, +preserved}:
700 construction_values_complete(dimensions, shape, preserved, Core.from_values(shape, values),
701 from_values_complete(shape, values,
702 %Equal.sym(List<&2, U32>, Shape.dimensions(shape), dimensions, preserved) :
703 {List.length(&2, F32, values) == Shape.logical_numel(_) : Nat}
704 counted))