ElementwisePROOF.loop_finish_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 371-391 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=371&end_line=391

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
import bendtorch-core@0.1.0.0/src/tensor/elementwise_totality.bend as Totality

def loop_finish_retains(+fuel: Nat, +operation: Elementwise.Operation, +plan: Shape.BroadcastPlan, +cursor: Nat,
  -left: Core.Dynamic, -right: Core.Dynamic, result: Elementwise.NaturalStep<Shape.output_shape(plan), cursor>,
  -sources: NaturalSources<Shape.output_shape(plan), cursor, left, right, result>,
  -rec: @state: Elementwise.State<Shape.output_shape(plan)> ->
    @-l: Totality.SameSource(left, step_left_owner(Shape.output_shape(plan), Elementwise.Continue{state})) ->
    @-r: Totality.SameSource(right, step_right_owner(Shape.output_shape(plan), Elementwise.Continue{state})) ->
    Totality.Retention<left, right, Elementwise.loop(fuel, operation, plan, 1n+cursor, state)>) ->
  Totality.Retention<left, right, Elementwise.finish_step(Shape.output_shape(plan), cursor,
    state => Elementwise.loop(fuel, operation, plan, 1n+cursor, state), result)>:
  match result:
    case Elementwise.NaturalStop{retained_left, retained_right, error}:
      Totality.Retention{
        {\{NaturalSources: l => r => l} : NaturalSources<Shape.output_shape(plan), cursor, left, right, Elementwise.NaturalStop{retained_left, retained_right, error}> -> Totality.SameSource(left, retained_left)}(sources),
        {\{NaturalSources: l => r => r} : NaturalSources<Shape.output_shape(plan), cursor, left, right, Elementwise.NaturalStop{retained_left, retained_right, error}> -> Totality.SameSource(right, retained_right)}(sources)}
    case Elementwise.NaturalContinue{state, index, exact}:
      retention_reify(left, right, Elementwise.loop(fuel, operation, plan, 1n+cursor, state),
        rec(state)(
          {\{NaturalSources: l => r => l} : NaturalSources<Shape.output_shape(plan), cursor, left, right, Elementwise.NaturalContinue{state, index, exact}> ->
            Totality.SameSource(left, step_left_owner(Shape.output_shape(plan), Elementwise.Continue{state}))}(sources))(
          {\{NaturalSources: l => r => r} : NaturalSources<Shape.output_shape(plan), cursor, left, right, Elementwise.NaturalContinue{state, index, exact}> ->
            Totality.SameSource(right, step_right_owner(Shape.output_shape(plan), Elementwise.Continue{state}))}(sources)))

Uses (16):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  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=output_shape
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/core.bend&name=Dynamic
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise.bend&name=NaturalStep
  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=finish_step
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise.bend&name=loop
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise_PROOF.bend&name=NaturalSources
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise_PROOF.bend&name=retention_reify
  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_right_owner
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise_totality.bend&name=Retention
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise_totality.bend&name=SameSource