ReductionPROOF.source_extend: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/tensor/reduction_PROOF.bend as ReductionPROOF
Lines 519-533 of bendtorch-core@0.1.0.0/src/tensor/reduction_PROOF.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/tensor/reduction_PROOF.bend&start_line=519&end_line=533

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/reduction_LAWS.bend as Laws

def source_extend(+fuel: Nat, -shape: Shape.Shape, -original: Core.Tensor<shape>, -tensor: Core.Tensor<shape>, +cursor: Nat,
  +accumulator: F32, +head: F32, result: Result<&2, &1, Core.Error, Core.Tensor<shape> & F32>,
  next: Laws.LoopMeaning(fuel, shape, tensor, 1n+cursor, F32.add(accumulator, head), result),
  -exact: {U32.to_nat(U32.from_nat(cursor)) == cursor : Nat},
  -observed: {Core.checked_observe(shape, original, U32.from_nat(cursor)) == Some{head} : Maybe<&2, F32>},
  -kept: @+other: U32 -> {Core.checked_observe(shape, tensor, other) == Core.checked_observe(shape, original, other) : Maybe<&2, F32>}) ->
  Laws.LoopMeaning(1n+fuel, shape, original, cursor, accumulator, result):
  match result:
    case Fail{error}:
      Unit{}
    case Done{pair}:
      (retained, value) = pair
      Laws.SumMeaning{values, logical, fold} = next
      Laws.SumMeaning{head <> values,
        Laws.LogicalStep{exact, observed, logical_original(fuel, shape, original, tensor, 1n+cursor, values, logical, kept)}, fold}

Uses (20):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=F32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=F32.add
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  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=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=Base/base.bend&name=U32.from_nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.to_nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Unit
  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=Tensor
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/core.bend&name=checked_observe
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/reduction_LAWS.bend&name=LogicalStep
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/reduction_LAWS.bend&name=LoopMeaning
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/reduction_LAWS.bend&name=SumMeaning
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/reduction_PROOF.bend&name=logical_original