TensorCursorWitness.read_stride: def of stelliferous@0.0.2.0
Import: import stelliferous@0.0.2.0/proofs/tensor_cursor_witness.bend as TensorCursorWitness
Lines 31-34 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=31&end_line=34

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_stride(~Element: Data,-storage: Array<Element>,cursor: Cursor.Stride,evidence: Witness.ArrayWitness<Element,storage>) ->
  VisitWitness.Sample<Array<Element>,Element,Cursor.Stride,storage,Cursor.read_stride(~Element,storage,cursor)>:
  Cursor.Stride{+address,+stride} = cursor
  stride_value(~Element,address,stride,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=stride_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=Stride
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/tensor_cursor.bend&name=read_stride