def finish

stelliferous@0.0.2.0 · proofs/traversal_witness.bend:61

import Base
import stelliferous@0.0.2.0/traversal_array.bend as Traversal

61def finish(~Reader: Type,~Element: Data,~Context: Data,-reader: Reader,-depth: Nat,
62  -state: Traversal.State<&1,&1,Reader,Array<Element>,Context>,evidence: StateEvidence<Reader,Element,Context,reader,depth,state>) ->
63  ResultEvidence<Reader,Element,reader,depth,Traversal.finish(~Reader,~Element,~Context,state)>:
64  match evidence:
65    case StateEvidence{output,position,context,equation,output_evidence}:
66      %Equal.sym(Traversal.State<&1,&1,Reader,Array<Element>,Context>,state,Traversal.State{reader,output,position,context},equation) :
67        ResultEvidence<Reader,Element,reader,depth,Traversal.finish(~Reader,~Element,~Context,_)>
68      ResultEvidence{output,{==},output_evidence}