def counted_from_values_success

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

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/shape/nat_proofs.bend as Nats
import bendtorch-core@0.1.0.0/src/tensor/allocation_PROOF.bend as AllocationProof

637def counted_from_values_success(+shape: Shape.Shape, +values: List<&2, F32>,
638  decision: Shape.BoolCase<Nat.is_eq(List.length(&2, F32, values), Shape.elements(shape))>,
639  counted: {List.length(&2, F32, values) == Shape.elements(shape) : Nat}) ->
640  FillSuccess<shape, Core.from_values_counted(shape, values, decision)>:
641  match decision:
642    case Shape.BFalse{equal}:
643      FillSuccess{Empty.absurd({False{} == True{} : Bool}, Nats.contradiction(Nat.is_eq(List.length(&2, F32, values), Shape.elements(shape)),
644        AllocationProof.natural_equal_true(List.length(&2, F32, values), Shape.elements(shape), counted), equal))}
645    case Shape.BTrue{equal}:
646      allocated_fill_success(shape, values, Core.new(shape, 0.0), AllocationProof.core_new_done(shape, 0.0), counted)