def read_success_model
bendtorch-core@0.1.0.0 · src/tensor/transform_PROOF.bend:1260
import bendtorch-core@0.1.0.0/src/tensor/transform_PROOF.bend as TransformPROOF
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
1260def read_success_model(-shape: Shape.Shape, -original: Core.Tensor<shape>, +index: U32,
1261 certificate: Core.Read<shape, original, index>,
1262 -model: Core.SourceRead<shape, original, index>, -present: PresentObservation<shape, original, index>) -> ReadSuccessModel<shape, original, index>:
1263 Core.Read{retained, result, exact} = certificate
1264 match result:
1265 case Fail{error}:
1266 ReadSuccessModel{Empty.absurd(ReadSuccess<shape, original, index>,
1267 {\{Core.SourceRead: meaning =>
1268 {\{PresentObservation: value => equal => Arith.clash(Equal.cong(Maybe<&2, F32>, Bool, maybe_present, None{}, Some{value},
1269 Equal.trans(Maybe<&2, F32>, None{}, Core.checked_observe(shape, original, index), Some{value},
1270 Equal.trans(Maybe<&2, F32>, None{}, Core.read_value(shape, Core.read_flat(shape, original, index)),
1271 Core.checked_observe(shape, original, index),
1272 Equal.cong(Core.Tensor<shape> & Result<&2, &2, Core.Error, F32>, Maybe<&2, F32>, pair => Core.read_value(shape, pair),
1273 (retained, Fail{error}), Core.read_flat(shape, original, index), exact), meaning), equal)))} :
1274 PresentObservation<shape, original, index> -> Empty}(present)} : Core.SourceRead<shape, original, index> -> Empty}(model))}
1275 case Done{value}:
1276 ReadSuccessModel{ReadSuccess{retained, value, exact}}