def read_stride
stelliferous@0.0.2.0 · proofs/tensor_cursor_witness.bend:31
import stelliferous@0.0.2.0/proofs/tensor_cursor_witness.bend as TensorCursorWitness
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
31def read_stride(~Element: Data,-storage: Array<Element>,cursor: Cursor.Stride,evidence: Witness.ArrayWitness<Element,storage>) ->
32 VisitWitness.Sample<Array<Element>,Element,Cursor.Stride,storage,Cursor.read_stride(~Element,storage,cursor)>:
33 Cursor.Stride{+address,+stride} = cursor
34 stride_value(~Element,address,stride,storage,Array.get(Element,storage,address),Witness.observed(Element,storage,address,evidence))