def output_witness
stelliferous@0.0.2.0 · proofs/traversal_witness.bend:98
import stelliferous@0.0.2.0/proofs/traversal_witness.bend as TraversalWitness
import Base
import stelliferous@0.0.2.0/proofs/storage_witness.bend as Witness
98def output_witness(~Reader: Type,~Element: Data,-reader: Reader,-depth: Nat,-result: Reader & Array<Element>,
99 evidence: ResultEvidence<Reader,Element,reader,depth,result>) -> Witness.Witness(Element,depth,second(~Reader,~Array<Element>,result)):
100 match evidence:
101 case ResultEvidence{output,equation,output_evidence}:
102 %Equal.sym(Reader & Array<Element>,result,(reader,output),equation) : Witness.Witness(Element,depth,second(~Reader,~Array<Element>,_))
103 output_evidence