GatherPROOF.split_facts: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/tensor/gather_PROOF.bend as GatherPROOF
Lines 331-334 of bendtorch-core@0.1.0.0/src/tensor/gather_PROOF.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/tensor/gather_PROOF.bend&start_line=331&end_line=334

import Base
import bendtorch-core@0.1.0.0/src/storage/model.bend as Model
import bendtorch-core@0.1.0.0/src/tensor/parallel_proofs.bend as Generic

def split_facts(+da: Nat, -A: Array<F32>, +di: Nat, -I: Array<U32>, -valid: Model.Balanced(F32, da, A), -index_valid: Model.Balanced(U32, di, I)) ->
  Generic.Fact<SplitFacts(A, I)>:
  Generic.Fact{{\{Generic.Fact: q => q} : Generic.Fact<SplitFacts(A, I)> -> SplitFacts(A, I)}(
    halves_facts(da, A, di, I, Array.clone(F32, A), Array.clone(U32, I), {==}, {==}, valid, index_valid))}

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=Array.clone
  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=Base/base.bend&name=U32
  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/gather_PROOF.bend&name=SplitFacts
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/gather_PROOF.bend&name=halves_facts
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/parallel_proofs.bend&name=Fact