ElementwisePROOF.dynamic_read_retains: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/tensor/elementwise_PROOF.bend as ElementwisePROOF
Lines 209-225 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=209&end_line=225

import Base
import bendtorch-core@0.1.0.0/src/storage/main.bend as Storage
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

def dynamic_read_retains(original: Core.Dynamic, +index: U32) -> SourceModel<original, dynamic_read_owner(Core.read_dynamic(original, index))>:
  Core.Packed{+shape, Core.TTensor{storage, exact}} = original
  match storage:
    case Storage.Empty{}:
      SourceModel{property => {\{InspectionModel: equal => equal} :
        InspectionModel<Totality.inspect(property, dynamic_read_owner(Core.read_dynamic(Core.Packed{shape, Core.TTensor{Storage.Empty{}, exact}}, index))),
          Totality.inspect(property, Core.Packed{shape, Core.TTensor{Storage.Empty{}, exact}})> ->
        {Totality.inspect(property, dynamic_read_owner(Core.read_dynamic(Core.Packed{shape, Core.TTensor{Storage.Empty{}, exact}}, index))) ==
          Totality.inspect(property, Core.Packed{shape, Core.TTensor{Storage.Empty{}, exact}}) : Totality.Inspection}}(
            empty_read_property(shape, index, property, exact))}
    case Storage.Owned{+depth, +length, array, balanced, valid}:
      SourceModel{property => {\{InspectionModel: equal => equal} :
        InspectionModel<Totality.inspect(property, dynamic_read_owner(Core.read_dynamic(Core.Packed{shape, Core.TTensor{Storage.Owned{depth, length, array, balanced, valid}, exact}}, index))),
          Totality.inspect(property, Core.Packed{shape, Core.TTensor{Storage.Owned{depth, length, array, balanced, valid}, exact}})> ->
        {Totality.inspect(property, dynamic_read_owner(Core.read_dynamic(Core.Packed{shape, Core.TTensor{Storage.Owned{depth, length, array, balanced, valid}, exact}}, index))) ==
          Totality.inspect(property, Core.Packed{shape, Core.TTensor{Storage.Owned{depth, length, array, balanced, valid}, exact}}) : Totality.Inspection}}(
            owned_read_property(shape, depth, length, index, property, array, balanced, valid, exact))}

Uses (12):
  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/storage/main.bend&name=Storage
  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=Tensor
  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/elementwise_PROOF.bend&name=InspectionModel
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise_PROOF.bend&name=SourceModel
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise_PROOF.bend&name=dynamic_read_owner
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise_PROOF.bend&name=empty_read_property
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise_PROOF.bend&name=owned_read_property
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise_totality.bend&name=Inspection
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise_totality.bend&name=inspect