def cell_keeps

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

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

632def cell_keeps(+plan: Slice.Plan, +at: Nat, +da: Nat, -A: Array<F32>, inside: Bool, -valid: Model.Balanced(F32, da, A)) ->
633  Parallel.Fact<{Pair.snd(F32, Array<F32> & Array<F32>, Slice.cell(plan, at, (A, empty()), inside)) == (A, empty()) : Array<F32> & Array<F32>}>:
634  match inside:
635    case False{}:
636      Parallel.Fact{{==}}
637    case True{}:
638      read_keeps(da, A, empty(), Slice.source(plan, at), valid)