def dynamic_read_success

bendtorch-core@0.1.0.0 · src/tensor/elementwise_PROOF.bend:588

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/elementwise_totality.bend as Totality
import bendtorch-core@0.1.0.0/src/tensor/transform_PROOF.bend as TransformProof
import bendtorch-core@0.1.0.0/src/tensor/transform_totality.bend as TransformTotality

588def dynamic_read_success(original: Core.Dynamic, +index: U32,
589  -inside: {Nat.is_lt(U32.to_nat(index), Shape.logical_numel(Totality.dimensions(original))) == True{} : Bool}) -> DynamicReadSuccess<original, index>:
590  Core.Packed{+shape, tensor} = original
591  DynamicReadSuccess{Equal.trans(Bool, dynamic_read_succeeded(Core.read_dynamic(Core.Packed{shape, tensor}, index)),
592    TransformTotality.read_succeeded(shape, Core.read_flat(shape, tensor, index)), True{},
593    dynamic_read_status(shape, Core.read_flat(shape, tensor, index)),
594    {\{TransformTotality.ReadSuccess: successful => successful} : TransformTotality.ReadSuccess<shape, tensor, index> ->
595      {TransformTotality.read_succeeded(shape, Core.read_flat(shape, tensor, index)) == True{} : Bool}}(
596        TransformProof.read_success_status(shape, tensor, index, TransformProof.read_success(shape, tensor, index, inside))))}