ElementwisePROOF.dynamic_read_success: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/tensor/elementwise_PROOF.bend as ElementwisePROOF
Lines 588-596 of bendtorch-core@0.1.0.0/src/tensor/elementwise_PROOF.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise_PROOF.bend&start_line=588&end_line=596

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

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

Uses (17):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_lt
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.to_nat
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=logical_numel
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/core.bend&name=Dynamic
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/core.bend&name=read_dynamic
  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/elementwise_PROOF.bend&name=DynamicReadSuccess
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise_PROOF.bend&name=dynamic_read_status
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise_PROOF.bend&name=dynamic_read_succeeded
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise_totality.bend&name=dimensions
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/transform_PROOF.bend&name=read_success
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/transform_PROOF.bend&name=read_success_status
  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