SlicePROOF.scatter_slot: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/tensor/slice_PROOF.bend as SlicePROOF
Lines 858-872 of bendtorch-core@0.1.0.0/src/tensor/slice_PROOF.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/tensor/slice_PROOF.bend&start_line=858&end_line=872

import Base
import bendtorch-core@0.1.0.0/src/storage/model.bend as Model
import bendtorch-core@0.1.0.0/src/tensor/slice.bend as Slice
import bendtorch-core@0.1.0.0/src/tensor/elementwise_parallel_proof.bend as Parallel

# The slot of input cell (o, i, r), below the count, holds what the gradient
# target of the cell names.
def scatter_slot(+depth: Nat, +splits: Nat, +plan: Slice.Plan, +count: Nat, +base: Nat, +dg: Nat, -G: Array<F32>, g: Array<F32>,
  -same: {g == G : Array<F32>}, -valid: Model.Balanced(F32, dg, G), +path: Model.Path(depth),
  -inside: {Nat.is_lt(Nat.add(Model.offset(depth, path), base), count) == True{} : Bool}) ->
  Parallel.Fact<{Model.observe(F32, depth, Slice.scatter_build(depth, splits, plan, count, base, g), path) ==
    Some{Pair.fst(F32, Array<F32> & Array<F32>, Slice.scattered((G, empty()), Slice.target(plan, Nat.add(Model.offset(depth, path), base))))} :
    Maybe<&2, F32>}>:
  Parallel.Fact{
    %inside :
      {Model.observe(F32, depth, Slice.scatter_build(depth, splits, plan, count, base, g), path) ==
        Some{Pair.fst(F32, Array<F32> & Array<F32>, Slice.scatter_cell(plan, Nat.add(Model.offset(depth, path), base), (G, empty()), _))} :
        Maybe<&2, F32>}
    {\{Parallel.Fact: q => q} : Parallel.Fact<ScatterCells(depth, splits, plan, count, base, G, g)> -> ScatterCells(depth, splits, plan, count, base, G, g)}(
      scatter_cells(depth, splits, plan, count, base, dg, G, g, same, valid))(path)}

Uses (23):
  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=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.add
  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=Sigma
  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=Path
  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/model.bend&name=offset
  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/slice.bend&name=Plan
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/slice.bend&name=scatter_build
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/slice.bend&name=scatter_cell
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/slice.bend&name=scattered
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/slice.bend&name=target
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/slice_PROOF.bend&name=ScatterCells
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/slice_PROOF.bend&name=empty
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/slice_PROOF.bend&name=scatter_cells