def scatter_keeps

bendtorch-core@0.1.0.0 · src/tensor/slice_PROOF.bend:648

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

648def scatter_keeps(+plan: Slice.Plan, +at: Nat, +da: Nat, -A: Array<F32>, inside: Bool, -valid: Model.Balanced(F32, da, A)) ->
649  Parallel.Fact<{Pair.snd(F32, Array<F32> & Array<F32>, Slice.scatter_cell(plan, at, (A, empty()), inside)) == (A, empty()) : Array<F32> & Array<F32>}>:
650  match inside:
651    case False{}:
652      Parallel.Fact{{==}}
653    case True{}:
654      scattered_keeps(da, A, Slice.target(plan, at), valid)