def read
stelliferous@0.0.2.0 · proofs/tensor_cursor_witness.bend:17
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
17def read(~Element: Data,-storage: Array<Element>,cursor: Cursor.Cursor,evidence: Witness.ArrayWitness<Element,storage>) ->
18 VisitWitness.Sample<Array<Element>,Element,Cursor.Cursor,storage,Cursor.read(~Element,storage,cursor)>:
19 Cursor.Cursor{axes,+address} = cursor
20 read_value(~Element,axes,address,storage,Array.get(Element,storage,address),Witness.observed(Element,storage,address,evidence))