ConstructionPROOF.counted_from_values_success: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/tensor/construction_PROOF.bend as ConstructionPROOF
Lines 637-646 of bendtorch-core@0.1.0.0/src/tensor/construction_PROOF.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/tensor/construction_PROOF.bend&start_line=637&end_line=646

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

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

Uses (17):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Empty.absurd
  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=Nat.is_eq
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=BoolCase
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=Shape
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=elements
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/nat_proofs.bend&name=contradiction
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/allocation_PROOF.bend&name=core_new_done
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/allocation_PROOF.bend&name=natural_equal_true
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/construction_PROOF.bend&name=FillSuccess
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/construction_PROOF.bend&name=allocated_fill_success
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/core.bend&name=from_values_counted
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/core.bend&name=new