TransformPROOF.read_success_status: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/tensor/transform_PROOF.bend as TransformPROOF
Lines 1452-1461 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=1452&end_line=1461

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

def read_success_status(-shape: Shape.Shape, -original: Core.Tensor<shape>, -index: U32,
  certificate: ReadSuccessModel<shape, original, index>) -> Totality.ReadSuccess<shape, original, index>:
  Totality.ReadSuccess{
    {\{ReadSuccessModel: success =>
      {\{ReadSuccess: retained => value => exact =>
        Equal.sym(Bool, True{}, Totality.read_succeeded(shape, Core.read_flat(shape, original, index)),
          Equal.cong(Core.Tensor<shape> & Result<&2, &2, Core.Error, F32>, Bool, Totality.read_succeeded(shape),
            (retained, Done{value}), Core.read_flat(shape, original, index), exact))} :
              ReadSuccess<shape, original, index> -> {Totality.read_succeeded(shape, Core.read_flat(shape, original, index)) == True{} : Bool}}(success)} :
                ReadSuccessModel<shape, original, index> -> {Totality.read_succeeded(shape, Core.read_flat(shape, original, index)) == True{} : Bool}}(certificate)}

Uses (16):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong
  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=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=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/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_totality.bend&name=ReadSuccess
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/transform_totality.bend&name=read_succeeded