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

import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/storage/main.bend as Storage
import bendtorch-core@0.1.0.0/src/storage/model.bend as Model
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 owned_read_property(+shape: Shape.Shape, +depth: Nat, +length: Nat, +index: U32, property: Totality.Property,
  -array: Array<F32>, -balanced: Model.Balanced(F32, depth, array), -valid: {Storage.bounds(depth, length) == True{} : Bool},
  -exact: {length == Shape.logical_numel(Shape.dimensions(shape)) : Nat}) ->
  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}})>:
  match property:
    case Totality.Dimensions{}:
      InspectionModel{Equal.trans(Totality.Inspection,
        Totality.inspect(Totality.Dimensions{}, dynamic_read_owner(Core.read_dynamic(Core.Packed{shape, Core.TTensor{Storage.Owned{depth, length, array, balanced, valid}, exact}}, index))),
        Totality.inspect(Totality.Dimensions{}, Core.Packed{shape, tensor_read_owner(shape, Core.read_flat(shape, Core.TTensor{Storage.Owned{depth, length, array, balanced, valid}, exact}, index))}),
        Totality.Dims{Shape.dimensions(shape)},
        dynamic_read_projection(shape, Totality.Dimensions{}, Core.read_flat(shape, Core.TTensor{Storage.Owned{depth, length, array, balanced, valid}, exact}, index)),
        tensor_read_dimensions(shape, Core.read_flat(shape, Core.TTensor{Storage.Owned{depth, length, array, balanced, valid}, exact}, index)))}
    case Totality.Checked{+other}:
      InspectionModel{Equal.trans(Totality.Inspection,
        Totality.inspect(Totality.Checked{other}, dynamic_read_owner(Core.read_dynamic(Core.Packed{shape, Core.TTensor{Storage.Owned{depth, length, array, balanced, valid}, exact}}, index))),
        storage_inspect(Totality.Checked{other}, read_owner(Storage.get(Storage.Owned{depth, length, array, balanced, valid}, index))),
        array_inspect(depth, length, Totality.Checked{other}, array),
        Equal.trans(Totality.Inspection,
          Totality.inspect(Totality.Checked{other}, dynamic_read_owner(Core.read_dynamic(Core.Packed{shape, Core.TTensor{Storage.Owned{depth, length, array, balanced, valid}, exact}}, index))),
          Totality.inspect(Totality.Checked{other}, Core.Packed{shape, tensor_read_owner(shape, Core.read_flat(shape, Core.TTensor{Storage.Owned{depth, length, array, balanced, valid}, exact}, index))}),
          storage_inspect(Totality.Checked{other}, read_owner(Storage.get(Storage.Owned{depth, length, array, balanced, valid}, index))),
          dynamic_read_projection(shape, Totality.Checked{other}, Core.read_flat(shape, Core.TTensor{Storage.Owned{depth, length, array, balanced, valid}, exact}, index)),
          core_read_projection(shape, Storage.Owned{depth, length, array, balanced, valid}, exact, index, Totality.Checked{other}, Storage.get(Storage.Owned{depth, length, array, balanced, valid}, index), {==})),
        {\{InspectionModel: equal => equal} :
          InspectionModel<storage_inspect(Totality.Checked{other}, read_owner(Storage.get(Storage.Owned{depth, length, array, balanced, valid}, index))),
            array_inspect(depth, length, Totality.Checked{other}, array)> ->
          {storage_inspect(Totality.Checked{other}, read_owner(Storage.get(Storage.Owned{depth, length, array, balanced, valid}, index))) ==
            array_inspect(depth, length, Totality.Checked{other}, array) : Totality.Inspection}}(
              read_checked_inspect(depth, length, index, Nat.is_lt(U32.to_nat(index), length), Totality.Checked{other}, array, {==}, balanced, valid)))}
    case Totality.Raw{+other}:
      InspectionModel{Equal.trans(Totality.Inspection,
        Totality.inspect(Totality.Raw{other}, dynamic_read_owner(Core.read_dynamic(Core.Packed{shape, Core.TTensor{Storage.Owned{depth, length, array, balanced, valid}, exact}}, index))),
        storage_inspect(Totality.Raw{other}, read_owner(Storage.get(Storage.Owned{depth, length, array, balanced, valid}, index))),
        array_inspect(depth, length, Totality.Raw{other}, array),
        Equal.trans(Totality.Inspection,
          Totality.inspect(Totality.Raw{other}, dynamic_read_owner(Core.read_dynamic(Core.Packed{shape, Core.TTensor{Storage.Owned{depth, length, array, balanced, valid}, exact}}, index))),
          Totality.inspect(Totality.Raw{other}, Core.Packed{shape, tensor_read_owner(shape, Core.read_flat(shape, Core.TTensor{Storage.Owned{depth, length, array, balanced, valid}, exact}, index))}),
          storage_inspect(Totality.Raw{other}, read_owner(Storage.get(Storage.Owned{depth, length, array, balanced, valid}, index))),
          dynamic_read_projection(shape, Totality.Raw{other}, Core.read_flat(shape, Core.TTensor{Storage.Owned{depth, length, array, balanced, valid}, exact}, index)),
          core_read_projection(shape, Storage.Owned{depth, length, array, balanced, valid}, exact, index, Totality.Raw{other}, Storage.get(Storage.Owned{depth, length, array, balanced, valid}, index), {==})),
        {\{InspectionModel: equal => equal} :
          InspectionModel<storage_inspect(Totality.Raw{other}, read_owner(Storage.get(Storage.Owned{depth, length, array, balanced, valid}, index))),
            array_inspect(depth, length, Totality.Raw{other}, array)> ->
          {storage_inspect(Totality.Raw{other}, read_owner(Storage.get(Storage.Owned{depth, length, array, balanced, valid}, index))) ==
            array_inspect(depth, length, Totality.Raw{other}, array) : Totality.Inspection}}(
              read_checked_inspect(depth, length, index, Nat.is_lt(U32.to_nat(index), length), Totality.Raw{other}, array, {==}, balanced, valid)))}

Uses (32):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Array
  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=F32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  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=Shape
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=dimensions
  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/storage/main.bend&name=Storage
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/main.bend&name=bounds
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/main.bend&name=get
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/model.bend&name=Balanced
  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/core.bend&name=read_flat
  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=array_inspect
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise_PROOF.bend&name=core_read_projection
  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=dynamic_read_projection
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise_PROOF.bend&name=read_checked_inspect
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise_PROOF.bend&name=read_owner
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise_PROOF.bend&name=storage_inspect
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise_PROOF.bend&name=tensor_read_dimensions
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise_PROOF.bend&name=tensor_read_owner
  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=Property
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise_totality.bend&name=inspect