ParallelProofs.join_facts: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/tensor/parallel_proofs.bend as ParallelProofs
Lines 103-115 of bendtorch-core@0.1.0.0/src/tensor/parallel_proofs.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/tensor/parallel_proofs.bend&start_line=103&end_line=115

import Base
import bendtorch-core@0.1.0.0/src/tensor/parallel.bend as Build

def join_facts(~P: Data, ~A: Type, ~B: Type, ~cell: @+p: P -> @+position: Nat -> (A & B) -> Bool -> F32 & (A & B),
  +p: P, -start: (A & B), +inner: Nat, +count: Nat, +base: Nat, -a: Array<F32>, high: Array<F32> & (A & B),
  -low: Fact<Cells(~P, ~A, ~B, ~cell, p, start, inner, count, base, a)>,
  -facts: Fact<TreeFacts(~P, ~A, ~B, ~cell, p, start, inner, count, Build.upper(inner, base), high)>) ->
  Fact<TreeFacts(~P, ~A, ~B, ~cell, p, start, 1n+inner, count, base, Build.join(~(A & B), a, high))>:
  (b, rest) = high
  Fact{(
    {\{Fact: q => q} : Fact<({Pair.snd(Array<F32>, (A & B), (b, rest)) == start : (A & B)})> -> {Pair.snd(Array<F32>, (A & B), (b, rest)) == start : (A & B)}}(
      facts_kept(~P, ~A, ~B, ~cell, p, start, inner, count, Build.upper(inner, base), (b, rest), facts)),
    {\{Fact: q => q} : Fact<(Cells(~P, ~A, ~B, ~cell, p, start, 1n+inner, count, base, ANode{a, b}))> ->
      Cells(~P, ~A, ~B, ~cell, p, start, 1n+inner, count, base, ANode{a, b})}(
      node_cells(~P, ~A, ~B, ~cell, p, start, inner, count, base, a, b, low,
        facts_cells(~P, ~A, ~B, ~cell, p, start, inner, count, Build.upper(inner, base), (b, rest), facts))))}

Uses (15):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Array
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  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=Pair
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Pair.snd
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Sigma
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/parallel.bend&name=join
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/parallel.bend&name=upper
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/parallel_proofs.bend&name=Cells
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/parallel_proofs.bend&name=Fact
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/parallel_proofs.bend&name=TreeFacts
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/parallel_proofs.bend&name=facts_cells
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/parallel_proofs.bend&name=facts_kept
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/parallel_proofs.bend&name=node_cells