def scattered_keeps
bendtorch-core@0.1.0.0 · src/tensor/slice_PROOF.bend:640
import bendtorch-core@0.1.0.0/src/tensor/slice_PROOF.bend as SlicePROOF
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
640def scattered_keeps(+da: Nat, -A: Array<F32>, at: Maybe<&2, Nat>, -valid: Model.Balanced(F32, da, A)) ->
641 Parallel.Fact<{Pair.snd(F32, Array<F32> & Array<F32>, Slice.scattered((A, empty()), at)) == (A, empty()) : Array<F32> & Array<F32>}>:
642 match at:
643 case None{}:
644 Parallel.Fact{{==}}
645 case Some{+index}:
646 read_keeps(da, A, empty(), index, valid)