def construction_shape_elements

bendtorch-core@0.1.0.0 · src/tensor/construction_PROOF.bend:366

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_LAWS.bend as Laws

366def construction_shape_elements(+dimensions: List<&2, U32>, +values: List<&2, F32>, result: Shape.ConstructResult<dimensions>) ->
367  ConstructionOutcome<values, Core.construct_shape(dimensions, values, result)>:
368  match result:
369    case Shape.SError{error}:
370      ConstructionOutcome{Unit{}}
371    case Shape.SBuilt{+shape, preserved}:
372      ConstructionOutcome{
373        {\{ConstructionOutcome: meaning => meaning} : ConstructionOutcome<values, Core.construct_values(shape, Core.from_values(shape, values))> ->
374          Laws.ConstructionMeaning(values, Core.construct_values(shape, Core.from_values(shape, values)))}(construction_values_elements(shape, values, Core.from_values(shape, values),
375            {\{Laws.FromValuesModel: meaning => meaning} : Laws.FromValuesModel<shape, values> ->
376              Laws.FromValuesMeaning(shape, values, Core.from_values(shape, values))}(Laws.public_from_values_elements(shape, values))))}