ElementwiseParallelProof.cell_keeps: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/tensor/elementwise_parallel_proof.bend as ElementwiseParallelProof
Lines 161-179 of bendtorch-core@0.1.0.0/src/tensor/elementwise_parallel_proof.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise_parallel_proof.bend&start_line=161&end_line=179

import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/storage/model.bend as Model
import bendtorch-core@0.1.0.0/src/tensor/elementwise.bend as Elementwise
import bendtorch-core@0.1.0.0/src/tensor/elementwise_walk_proof.bend as WalkProof

# Every cell hands both input arrays back.
def cell_keeps(+operation: Elementwise.Operation, +plan: Shape.BroadcastPlan, +dl: Nat, +dr: Nat, -A: Array<F32>, -B: Array<F32>, +position: Nat,
  inside: Bool, -left_valid: Model.Balanced(F32, dl, A), -right_valid: Model.Balanced(F32, dr, B)) ->
  Fact<{Pair.snd(F32, Array<F32> & Array<F32>, cell_of(operation, plan, position, A, B, inside)) == (A, B) : Array<F32> & Array<F32>}>:
  match inside:
    case False{}:
      Fact{
        %Equal.sym(F32 & (Array<F32> & Array<F32>), cell_of(operation, plan, position, A, B, False{}),
          Elementwise.cell(operation, Shape.extents(Shape.left_shape(plan)), Shape.extents(Shape.right_shape(plan)),
            Shape.extents(Shape.output_shape(plan)), Shape.index_map(plan), position, A, B, False{}),
          WalkProof.cell_at_walk(operation, plan, position, A, B, False{})) :
          {Pair.snd(F32, Array<F32> & Array<F32>, _) == (A, B) : Array<F32> & Array<F32>}
        {==}}
    case True{}:
      Fact{Pair.fst({Pair.snd(F32, Array<F32> & Array<F32>, cell_of(operation, plan, position, A, B, True{})) == (A, B) : Array<F32> & Array<F32>},
        {Some{Pair.fst(F32, Array<F32> & Array<F32>, cell_of(operation, plan, position, A, B, True{}))} == want(operation, plan, dl, dr, A, B, position) : Maybe<&2, F32>},
        {\{Fact: q => q} : Fact<(CellOut(operation, plan, dl, dr, A, B, position, cell_of(operation, plan, position, A, B, True{})))> ->
          CellOut(operation, plan, dl, dr, A, B, position, cell_of(operation, plan, position, A, B, True{}))}(
          cell_out(operation, plan, dl, dr, A, B, position, left_valid, right_valid)))}

Uses (25):
  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=Equal.sym
  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=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/shape/core.bend&name=BroadcastPlan
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=extents
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=index_map
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=left_shape
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=output_shape
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=right_shape
  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=Operation
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise.bend&name=cell
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise_parallel_proof.bend&name=CellOut
  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=cell_of
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise_parallel_proof.bend&name=cell_out
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise_parallel_proof.bend&name=want
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise_walk_proof.bend&name=cell_at_walk