ParallelProofs.node_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 117-128 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=117&end_line=128

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

def node_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, rec: A -> B -> Array<F32> & (A & B), low: Array<F32> & (A & B),
  -facts: Fact<TreeFacts(~P, ~A, ~B, ~cell, p, start, inner, count, base, low)>,
  -next: @l: A -> @r: B -> @-at: {(l, r) == start : (A & B)} ->
    Fact<TreeFacts(~P, ~A, ~B, ~cell, p, start, inner, count, Build.upper(inner, base), rec(l, r))>) ->
  Fact<TreeFacts(~P, ~A, ~B, ~cell, p, start, 1n+inner, count, base, Build.node(~A, ~B, rec, low))>:
  (a, s) = low
  (l, r) = s
  join_facts(~P, ~A, ~B, ~cell, p, start, inner, count, base, a, rec(l, r),
    facts_cells(~P, ~A, ~B, ~cell, p, start, inner, count, base, (a, (l, r)), facts),
    next(l)(r)({\{Fact: q => q} : Fact<({Pair.snd(Array<F32>, (A & B), (a, (l, r))) == start : (A & B)})> -> {Pair.snd(Array<F32>, (A & B), (a, (l, r))) == start : (A & B)}}(
      facts_kept(~P, ~A, ~B, ~cell, p, start, inner, count, base, (a, (l, r)), facts))))

Uses (14):
  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=node
  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=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=join_facts