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

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/storage/arith.bend as Arith

def read_success_model(-shape: Shape.Shape, -original: Core.Tensor<shape>, +index: U32,
  certificate: Core.Read<shape, original, index>,
  -model: Core.SourceRead<shape, original, index>, -present: PresentObservation<shape, original, index>) -> ReadSuccessModel<shape, original, index>:
  Core.Read{retained, result, exact} = certificate
  match result:
    case Fail{error}:
      ReadSuccessModel{Empty.absurd(ReadSuccess<shape, original, index>,
        {\{Core.SourceRead: meaning =>
          {\{PresentObservation: value => equal => Arith.clash(Equal.cong(Maybe<&2, F32>, Bool, maybe_present, None{}, Some{value},
            Equal.trans(Maybe<&2, F32>, None{}, Core.checked_observe(shape, original, index), Some{value},
              Equal.trans(Maybe<&2, F32>, None{}, Core.read_value(shape, Core.read_flat(shape, original, index)),
                Core.checked_observe(shape, original, index),
                Equal.cong(Core.Tensor<shape> & Result<&2, &2, Core.Error, F32>, Maybe<&2, F32>, pair => Core.read_value(shape, pair),
                  (retained, Fail{error}), Core.read_flat(shape, original, index), exact), meaning), equal)))} :
                    PresentObservation<shape, original, index> -> Empty}(present)} : Core.SourceRead<shape, original, index> -> Empty}(model))}
    case Done{value}:
      ReadSuccessModel{ReadSuccess{retained, value, exact}}

Uses (24):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Empty
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Empty.absurd
  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.trans
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=F32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Maybe
  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/storage/arith.bend&name=clash
  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=Read
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/core.bend&name=SourceRead
  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/core.bend&name=read_flat
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/core.bend&name=read_value
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/transform_PROOF.bend&name=PresentObservation
  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=maybe_present