def read_success_status

bendtorch-core@0.1.0.0 · src/tensor/transform_PROOF.bend:1452

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

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