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

import Base
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/storage/refinement.bend as Refinement
import bendtorch-core@0.1.0.0/src/tensor/elementwise_totality.bend as Totality

def read_hit_inspect(+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}) ->
  InspectionModel<storage_inspect(property, read_owner(Storage.finish_read(depth, length, array, index, Array.get(F32, array, index), {==}, balanced, valid))),
    array_inspect(depth, length, property, array)>:
  match property:
    case Totality.Dimensions{}:
      InspectionModel{finish_read_inspect(depth, length, array, index, Totality.Dimensions{}, Array.get(F32, array, index), {==}, balanced, valid)}
    case Totality.Checked{+other}:
      InspectionModel{Equal.trans(Totality.Inspection,
        storage_inspect(Totality.Checked{other}, read_owner(Storage.finish_read(depth, length, array, index, Array.get(F32, array, index), {==}, balanced, valid))),
        array_inspect(depth, length, Totality.Checked{other}, Refinement.first(F32, Array.get(F32, array, index))),
        array_inspect(depth, length, Totality.Checked{other}, array),
        finish_read_inspect(depth, length, array, index, Totality.Checked{other}, Array.get(F32, array, index), {==}, balanced, valid),
        Equal.cong(Array<F32>, Totality.Inspection, a => array_inspect(depth, length, Totality.Checked{other}, a),
          Refinement.first(F32, Array.get(F32, array, index)), array, Refinement.law_get_retains(F32, depth, array, index, balanced)))}
    case Totality.Raw{+other}:
      InspectionModel{Equal.trans(Totality.Inspection,
        storage_inspect(Totality.Raw{other}, read_owner(Storage.finish_read(depth, length, array, index, Array.get(F32, array, index), {==}, balanced, valid))),
        array_inspect(depth, length, Totality.Raw{other}, Refinement.first(F32, Array.get(F32, array, index))),
        array_inspect(depth, length, Totality.Raw{other}, array),
        finish_read_inspect(depth, length, array, index, Totality.Raw{other}, Array.get(F32, array, index), {==}, balanced, valid),
        Equal.cong(Array<F32>, Totality.Inspection, a => array_inspect(depth, length, Totality.Raw{other}, a),
          Refinement.first(F32, Array.get(F32, array, index)), array, Refinement.law_get_retains(F32, depth, array, index, balanced)))}

Uses (20):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Array
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Array.get
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong
  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=U32
  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=finish_read
  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/storage/refinement.bend&name=first
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/refinement.bend&name=law_get_retains
  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=finish_read_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_totality.bend&name=Inspection
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise_totality.bend&name=Property