def indexed_sample
stelliferous@0.0.2.0 · proofs/tensor_access_certificate.bend:282
import stelliferous@0.0.2.0/proofs/tensor_access_certificate.bend as TensorAccessCertificate
import Base
import stelliferous@0.0.2.0/tensor_access.bend as Access
import stelliferous@0.0.2.0/proofs/traversal_witness.bend as TraversalWitness
282def indexed_sample(~Element: Data,~operation: U32 -> Element -> Element,-storage: Array<Element>,+position: U32,-result: Array<Element> & Element,
283 sample: TraversalWitness.Sample<Array<Element>,Element,storage,result>) ->
284 TraversalWitness.Sample<Array<Element>,Element,storage,Access.indexed_value(~Element,~operation,position,result)>:
285 match sample:
286 case TraversalWitness.Sample{value,equation}:
287 %Equal.sym(Array<Element> & Element,result,(storage,value),equation) :
288 TraversalWitness.Sample<Array<Element>,Element,storage,Access.indexed_value(~Element,~operation,position,_)>
289 TraversalWitness.Sample{operation(position,value),{==}}