ReduceParallelProof.leaf_run: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/autograd/reduce_parallel_proof.bend as ReduceParallelProof
Lines 282-294 of bendtorch-core@0.1.0.0/src/autograd/reduce_parallel_proof.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_parallel_proof.bend&start_line=282&end_line=294

import Base
import bendtorch-core@0.1.0.0/src/storage/model.bend as Model
import bendtorch-core@0.1.0.0/src/storage/refinement.bend as Refinement
import bendtorch-core@0.1.0.0/src/tensor/elementwise_parallel_proof.bend as Parallel
import bendtorch-core@0.1.0.0/src/autograd/reduce.bend as Reduce

def leaf_run(+d: Nat, -A: Array<F32>, +base: Nat, -accumulator: F32, -array: Array<F32>, pair: Array<F32> & F32,
  -exact: {pair == Array.get(F32, array, U32.from_nat(base)) : Array<F32> & F32}, -same: {array == A : Array<F32>},
  -valid: Model.Balanced(F32, d, A)) ->
  Parallel.Fact<FiberRun<d, A, [base], accumulator, Reduce.leaf_add(accumulator, pair)>>:
  (kept, word) = pair
  Parallel.Fact{FiberRun{[word],
    ObsStep{Equal.sym(Maybe<&2, F32>, Some{word}, Model.observe(F32, d, A, Refinement.route(d, U32.from_nat(base))),
      {\{Parallel.Fact: p => p} : Parallel.Fact<{Some{Refinement.second(F32, (kept, word))} == Model.observe(F32, d, A, Refinement.route(d, U32.from_nat(base))) : Maybe<&2, F32>}> ->
        {Some{Refinement.second(F32, (kept, word))} == Model.observe(F32, d, A, Refinement.route(d, U32.from_nat(base))) : Maybe<&2, F32>}}(
        Parallel.read_value(d, array, A, U32.from_nat(base), (kept, word), exact, same, valid))), Unit{}},
    {==},
    {\{Parallel.Fact: p => p} : Parallel.Fact<{Refinement.first(F32, (kept, word)) == A : Array<F32>}> -> {Refinement.first(F32, (kept, word)) == A : Array<F32>}}(
      Parallel.read_keeps(d, array, A, U32.from_nat(base), (kept, word), exact, same, valid))}}

Uses (22):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Array
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Array.get
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=F32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  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=Pair
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Sigma
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.from_nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Unit
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce.bend&name=leaf_add
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_parallel_proof.bend&name=FiberRun
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_parallel_proof.bend&name=ObsStep
  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/storage/model.bend&name=observe
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/refinement.bend&name=first
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/refinement.bend&name=route
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/refinement.bend&name=second
  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=read_keeps
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise_parallel_proof.bend&name=read_value