SlicePROOF.split_facts: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/tensor/slice_PROOF.bend as SlicePROOF
Lines 660-662 of bendtorch-core@0.1.0.0/src/tensor/slice_PROOF.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/tensor/slice_PROOF.bend&start_line=660&end_line=662

import Base
import bendtorch-core@0.1.0.0/src/storage/model.bend as Model
import bendtorch-core@0.1.0.0/src/tensor/elementwise_parallel_proof.bend as Parallel
import bendtorch-core@0.1.0.0/src/storage/array.bend as ArrayCore

def split_facts(+da: Nat, -A: Array<F32>, -valid: Model.Balanced(F32, da, A)) -> Parallel.Fact<SplitFacts(A)>:
  Parallel.Fact{{\{Parallel.Fact: q => q} : Parallel.Fact<SplitFacts(A)> -> SplitFacts(A)}(
    Parallel.split_equal(da, 0n, A, empty(), valid, ArrayCore.new_balanced(F32, 0n, 0.0)))}

Uses (9):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Array
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=F32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/array.bend&name=new_balanced
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/model.bend&name=Balanced
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise_parallel_proof.bend&name=Fact
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise_parallel_proof.bend&name=split_equal
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/slice_PROOF.bend&name=SplitFacts
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/slice_PROOF.bend&name=empty