def read_value
stelliferous@0.0.2.0 · proofs/tensor_cursor_witness.bend:8
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
8def read_value(~Element: Data,axes: Cursor.Levels(),address: U32,-storage: Array<Element>,-result: Array<Element> & Element,
9 observed: Witness.Read<Element,storage,result>) ->
10 VisitWitness.Sample<Array<Element>,Element,Cursor.Cursor,storage,Cursor.read_value(~Element,axes,address,result)>:
11 match observed:
12 case Witness.Read{value,equation}:
13 %Equal.sym(Array<Element> & Element,result,(storage,value),equation) :
14 VisitWitness.Sample<Array<Element>,Element,Cursor.Cursor,storage,Cursor.read_value(~Element,axes,address,_)>
15 VisitWitness.Sample{Cursor.advance(axes,address),value,{==}}