def witness_at
stelliferous@0.0.2.0 · proofs/storage_certificate.bend:61
import stelliferous@0.0.2.0/proofs/storage_certificate.bend as StorageCertificate
import Base
import stelliferous@0.0.2.0/proofs/storage_tree_model.bend as Tree
import stelliferous@0.0.2.0/proofs/storage_witness.bend as Witness
61def witness_at(-Element: Data,+depth: Nat,-storage: Array<Element>,
62 equation: {storage == Tree.pack(Element,normalized(Element,depth,Tree.reflect(Element,storage))) : Array<Element>}) ->
63 Witness.Witness(Element,depth,storage):
64 %Equal.sym(Array<Element>,storage,Tree.pack(Element,normalized(Element,depth,Tree.reflect(Element,storage))),equation) :
65 Witness.Witness(Element,depth,_)
66 normalized_witness(Element,depth,Tree.reflect(Element,storage))