TransformPROOF.copy_value_success: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/tensor/transform_PROOF.bend as TransformPROOF
Lines 1791-1809 of bendtorch-core@0.1.0.0/src/tensor/transform_PROOF.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/tensor/transform_PROOF.bend&start_line=1791&end_line=1809

import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/tensor/layout.bend as Layout
import bendtorch-core@0.1.0.0/src/tensor/core.bend as Core
import bendtorch-core@0.1.0.0/src/tensor/transforms.bend as Transforms
import bendtorch-core@0.1.0.0/src/storage/arith.bend as Arith
import bendtorch-core@0.1.0.0/src/tensor/word_conversion.bend as WordConversion
import bendtorch-core@0.1.0.0/src/tensor/transform_totality.bend as Totality

def copy_value_success(+input: Shape.Shape, +axes: List<&2, U32>, +plan: Layout.Plan<input, axes>, +index: U32,
  -source: Core.Tensor<input>, target: Core.Tensor<Layout.output(input, axes, plan)>, +value: F32,
  +inside: {True{} == U32.is_lt(index, Shape.count(Layout.output(input, axes, plan))) : Bool}) ->
  Totality.CopySuccess<input, axes, plan, Transforms.copy_read(input, axes, plan, index,
    source => target => (source, Done{target}), target, (source, Done{value}))>:
  copy_written_success(input, axes, plan, Core.write_flat(Layout.output(input, axes, plan), target, index, value), source,
    {\{Totality.WriteSuccess: successful => successful} :
      Totality.WriteSuccess<Layout.output(input, axes, plan), target, index, value> ->
        {Totality.write_succeeded(Layout.output(input, axes, plan), Core.write_flat(Layout.output(input, axes, plan), target, index, value)) == True{} : Bool}}(
          tensor_write_success(Layout.output(input, axes, plan), target, index, value,
            Equal.sym(Bool, True{}, Nat.is_lt(U32.to_nat(index), Shape.logical_numel(Shape.dimensions(Layout.output(input, axes, plan)))),
              %Shape.elements_exact(Layout.output(input, axes, plan)) :
                {True{} == Nat.is_lt(U32.to_nat(index), _) : Bool}
              %WordConversion.shape_count_exact(Layout.output(input, axes, plan)) :
                {True{} == Nat.is_lt(U32.to_nat(index), _) : Bool}
              %Equal.sym(Bool, Nat.is_lt(U32.to_nat(index), U32.to_nat(Shape.count(Layout.output(input, axes, plan)))),
                U32.is_lt(index, Shape.count(Layout.output(input, axes, plan))), Arith.u32_lt(index, Shape.count(Layout.output(input, axes, plan)))) :
                  {True{} == _ : Bool}
              inside))))

Uses (27):
  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=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_lt
  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.is_lt
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.to_nat
  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/shape/core.bend&name=count
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=dimensions
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=elements_exact
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=logical_numel
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/arith.bend&name=u32_lt
  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=write_flat
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/layout.bend&name=Plan
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/layout.bend&name=output
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/transform_PROOF.bend&name=copy_written_success
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/transform_PROOF.bend&name=tensor_write_success
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/transform_totality.bend&name=CopySuccess
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/transform_totality.bend&name=WriteSuccess
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/transform_totality.bend&name=write_succeeded
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/transforms.bend&name=copy_read
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/word_conversion.bend&name=shape_count_exact