~/jendhub

def read_index

stelliferous@0.0.2.0 · proofs/tensor_access_certificate.bend:17

import stelliferous@0.0.2.0/proofs/tensor_access_certificate.bend as TensorAccessCertificate
import Base
import stelliferous@0.0.2.0/traversal_array.bend as Traversal
import stelliferous@0.0.2.0/proofs/storage_witness.bend as Witness
import stelliferous@0.0.2.0/proofs/traversal_witness.bend as TraversalWitness

17def read_index(~Element: Data,-input: Array<Element>,context: Unit,index: U32,evidence: Witness.ArrayWitness<Element,input>) ->
18  TraversalWitness.Sample<Array<Element>,Element,input,Traversal.read_index(~Element,input,context,index)>:
19  TraversalWitness.array_sample(~Element,input,Array.get(Element,input,index),Witness.observed(Element,input,index,evidence))

Uses (9)

Used by (1)