ParallelProofs.leaf_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 59-69 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=59&end_line=69

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

def leaf_facts(~P: Data, ~A: Type, ~B: Type, ~cell: @+p: P -> @+position: Nat -> (A & B) -> Bool -> F32 & (A & B),
  +p: P, -start: (A & B), +count: Nat, +base: Nat, pair: F32 & (A & B),
  -exact: {pair == cell(p, base, start, Nat.is_lt(base, count)) : F32 & (A & B)},
  -keeps: Keeps(~P, ~A, ~B, ~cell, p, start)) ->
  Fact<TreeFacts(~P, ~A, ~B, ~cell, p, start, 0n, count, base, Build.leaf(~(A & B), pair))>:
  (value, rest) = pair
  Fact{(Equal.trans((A & B), rest, Pair.snd(F32, (A & B), cell(p, base, start, Nat.is_lt(base, count))), start,
      Equal.cong(F32 & (A & B), (A & B), q => Pair.snd(F32, (A & B), q), (value, rest), cell(p, base, start, Nat.is_lt(base, count)), exact),
      keeps(base)(Nat.is_lt(base, count))),
    path => Equal.cong(F32 & (A & B), Maybe<&2, F32>, q => Some{Pair.fst(F32, (A & B), q)}, (value, rest),
      cell(p, base, start, Nat.is_lt(base, count)), exact))}

Uses (15):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=F32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Maybe
  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_lt
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Pair
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Pair.fst
  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=leaf
  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=Keeps
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/parallel_proofs.bend&name=TreeFacts