def from_values_counted_elements

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

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

510def from_values_counted_elements(+shape: Shape.Shape, +values: List<&2, F32>,
511  decision: Shape.BoolCase<Nat.is_eq(List.length(&2, F32, values), Shape.elements(shape))>) ->
512  ElementsOutcome<shape, values, Core.from_values_counted(shape, values, decision)>:
513  match decision:
514    case Shape.BFalse{equal}:
515      ElementsOutcome{Unit{}}
516    case Shape.BTrue{equal}:
517      ElementsOutcome{
518        {\{ElementsOutcome: meaning => meaning} : ElementsOutcome<shape, values, Core.from_values_new(shape, values, Core.new(shape, 0.0))> ->
519          Laws.FromValuesMeaning(shape, values, Core.from_values_new(shape, values, Core.new(shape, 0.0)))}(from_values_new_elements(shape, values, Core.new(shape, 0.0), supplied_count(shape, values, equal)))}