SlicePROOF.scatter_cells: def of bendtorch-core@0.1.0.0 Import: import bendtorch-core@0.1.0.0/src/tensor/slice_PROOF.bend as SlicePROOF Lines 690-711 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=690&end_line=711 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.bend as Elementwise import bendtorch-core@0.1.0.0/src/tensor/elementwise_parallel_proof.bend as Parallel import bendtorch-core@0.1.0.0/src/tensor/parallel_proofs.bend as Generic def scatter_cells(+depth: Nat, +splits: Nat, +plan: Slice.Plan, +count: Nat, +base: Nat, +da: Nat, -A: Array, a: Array, -same: {a == A : Array}, -valid: Model.Balanced(F32, da, A)) -> Parallel.Fact, ~Array, ~Slice.scatter_cell, plan, (A, empty()), depth, count, base, Slice.scatter_build(depth, splits, plan, count, base, a))>: Parallel.Fact{path => {\{Generic.Fact: q => q} : Generic.Fact, ~Array, ~Slice.scatter_cell, plan, (A, empty()), depth, count, base, Slice.scatter_build(depth, splits, plan, count, base, a))> -> Generic.Cells(~Slice.Plan, ~Array, ~Array, ~Slice.scatter_cell, plan, (A, empty()), depth, count, base, Slice.scatter_build(depth, splits, plan, count, base, a))}( Generic.build_cells(~Slice.Plan, ~Slice.Plan, ~Array, ~Array, ~Slice.same, ~Elementwise.split, ~Slice.scatter_cell, plan, (A, empty()), depth, splits, count, base, (a, empty()), Parallel.pair_equal(a, empty(), A, empty(), same, {==}), at => inside => {\{Parallel.Fact: q => q} : Parallel.Fact<{Pair.snd(F32, Array & Array, Slice.scatter_cell(plan, at, (A, empty()), inside)) == (A, empty()) : Array & Array}> -> {Pair.snd(F32, Array & Array, Slice.scatter_cell(plan, at, (A, empty()), inside)) == (A, empty()) : Array & Array}}( scatter_keeps(plan, at, da, A, inside, valid)), Pair.fst({Pair.fst(Array & Array, Array & Array, Elementwise.split((A, empty()))) == (A, empty()) : Array & Array}, {Pair.snd(Array & Array, Array & Array, Elementwise.split((A, empty()))) == (A, empty()) : Array & Array}, {\{Parallel.Fact: q => q} : Parallel.Fact -> SplitFacts(A)}(split_facts(da, A, valid))), Pair.snd({Pair.fst(Array & Array, Array & Array, Elementwise.split((A, empty()))) == (A, empty()) : Array & Array}, {Pair.snd(Array & Array, Array & Array, Elementwise.split((A, empty()))) == (A, empty()) : Array & Array}, {\{Parallel.Fact: q => q} : Parallel.Fact -> SplitFacts(A)}(split_facts(da, A, valid)))))(path)} 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=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.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/storage/model.bend&name=Balanced https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise.bend&name=split 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=pair_equal 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=build_cells 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=same 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_PROOF.bend&name=SplitFacts 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_keeps https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/slice_PROOF.bend&name=split_facts