TensorCursorWitness.read: def of stelliferous@0.0.2.0
Import: import stelliferous@0.0.2.0/proofs/tensor_cursor_witness.bend as TensorCursorWitness
Lines 17-20 of stelliferous@0.0.2.0/proofs/tensor_cursor_witness.bend: https://jend.leeeet.dev/read.txt?path=stelliferous@0.0.2.0/proofs/tensor_cursor_witness.bend&start_line=17&end_line=20

import Base
import stelliferous@0.0.2.0/tensor_cursor.bend as Cursor
import stelliferous@0.0.2.0/proofs/storage_witness.bend as Witness
import stelliferous@0.0.2.0/proofs/traversal_visit_witness.bend as VisitWitness

def read(~Element: Data,-storage: Array<Element>,cursor: Cursor.Cursor,evidence: Witness.ArrayWitness<Element,storage>) ->
  VisitWitness.Sample<Array<Element>,Element,Cursor.Cursor,storage,Cursor.read(~Element,storage,cursor)>:
  Cursor.Cursor{axes,+address} = cursor
  read_value(~Element,axes,address,storage,Array.get(Element,storage,address),Witness.observed(Element,storage,address,evidence))

Uses (8):
  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=stelliferous@0.0.2.0/proofs/storage_witness.bend&name=ArrayWitness
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/storage_witness.bend&name=observed
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/tensor_cursor_witness.bend&name=read_value
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/traversal_visit_witness.bend&name=Sample
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/tensor_cursor.bend&name=Cursor
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/tensor_cursor.bend&name=read