TransformPROOF.copy_read_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 1811-1833 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=1811&end_line=1833

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/tensor/transform_totality.bend as Totality

def copy_read_success(+input: Shape.Shape, +axes: List<&2, U32>, +plan: Layout.Plan<input, axes>, +index: U32, +source_index: U32,
  -source: Core.Tensor<input>, target: Core.Tensor<Layout.output(input, axes, plan)>,
  certificate: ReadSuccessModel<input, source, source_index>,
  +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, Core.read_flat(input, source, source_index))>:
  Totality.CopySuccess{
    {\{ReadSuccessModel: success =>
      {\{ReadSuccess: retained => value => exact =>
        %exact : {Totality.copy_succeeded(input, axes, plan, Transforms.copy_read(input, axes, plan, index,
          source => target => (source, Done{target}), target, _)) == True{} : Bool}
        {\{Totality.CopySuccess: successful => successful} :
          Totality.CopySuccess<input, axes, plan, Transforms.copy_read(input, axes, plan, index,
            source => target => (source, Done{target}), target, (retained, Done{value}))> ->
              {Totality.copy_succeeded(input, axes, plan, Transforms.copy_read(input, axes, plan, index,
                source => target => (source, Done{target}), target, (retained, Done{value}))) == True{} : Bool}}(
                  copy_value_success(input, axes, plan, index, retained, target, value, inside))} :
                    ReadSuccess<input, source, source_index> ->
                      {Totality.copy_succeeded(input, axes, plan, Transforms.copy_read(input, axes, plan, index,
                        source => target => (source, Done{target}), target, Core.read_flat(input, source, source_index))) == True{} : Bool}}(success)} :
                          ReadSuccessModel<input, source, source_index> ->
                            {Totality.copy_succeeded(input, axes, plan, Transforms.copy_read(input, axes, plan, index,
                              source => target => (source, Done{target}), target, Core.read_flat(input, source, source_index))) == True{} : Bool}}(certificate)}

Uses (18):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  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=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/tensor/core.bend&name=Tensor
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/core.bend&name=read_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=ReadSuccess
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/transform_PROOF.bend&name=ReadSuccessModel
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/transform_PROOF.bend&name=copy_value_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=copy_succeeded
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/transforms.bend&name=copy_read