ElementwisePROOF.step_indices_retains: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/tensor/elementwise_PROOF.bend as ElementwisePROOF
Lines 298-315 of bendtorch-core@0.1.0.0/src/tensor/elementwise_PROOF.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise_PROOF.bend&start_line=298&end_line=315

import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/tensor/core.bend as Core
import bendtorch-core@0.1.0.0/src/tensor/elementwise.bend as Elementwise

def step_indices_retains(+operation: Elementwise.Operation, -shape: Shape.Shape, +index: U32,
  state: Elementwise.State<shape>, result: Result<&2, &1, Core.Error, U32 & U32>) ->
  StepSources<shape,
    step_left_owner(shape, Elementwise.Continue{state}), step_right_owner(shape, Elementwise.Continue{state}),
    Elementwise.step_indices(operation, shape, index, state, result)>:
  Elementwise.State{left, right, output} = state
  match result:
    case Fail{error}:
      StepSources{property => {==}, property => {==}}
    case Done{indices}:
      (+left_index, +right_index) = indices
      step_sources_reify(shape, left, right,
        Elementwise.step_left(operation, shape, index, right, output, right_index, Core.read_dynamic(left, left_index)),
        {\{SourceModel: same => step_left_retains(operation, shape, index, left, right, right, output, right_index,
        Core.read_dynamic(left, left_index), same, property => {==})} :
        SourceModel<left, dynamic_read_owner(Core.read_dynamic(left, left_index))> ->
        StepSources<shape, left, right, Elementwise.step_left(operation, shape, index, right, output, right_index, Core.read_dynamic(left, left_index))>}(
          dynamic_read_retains(left, left_index)))

Uses (20):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Pair
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Result
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Sigma
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=Shape
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/core.bend&name=Error
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/core.bend&name=read_dynamic
  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=State
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise.bend&name=Step
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise.bend&name=step_indices
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise.bend&name=step_left
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise_PROOF.bend&name=SourceModel
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise_PROOF.bend&name=StepSources
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise_PROOF.bend&name=dynamic_read_owner
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise_PROOF.bend&name=dynamic_read_retains
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise_PROOF.bend&name=step_left_owner
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise_PROOF.bend&name=step_left_retains
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise_PROOF.bend&name=step_right_owner
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise_PROOF.bend&name=step_sources_reify