def fold_finished

stelliferous@0.0.2.0 · proofs/traversal_witness.bend:268

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

268def fold_finished(~Reader: Type,~Accumulator: Data,~Context: Data,-reader: Reader,
269  -state: Traversal.State<&1,&2,Reader,Accumulator,Context>,evidence: FoldEvidence<Reader,Accumulator,Context,reader,state>) ->
270  {first(~Reader,~Accumulator,Traversal.finish_fold(~Reader,~Accumulator,~Context,state)) == reader : Reader}:
271  match evidence:
272    case FoldEvidence{accumulator,position,context,equation}:
273      %Equal.sym(Traversal.State<&1,&2,Reader,Accumulator,Context>,state,Traversal.State{reader,accumulator,position,context},equation) :
274        {first(~Reader,~Accumulator,Traversal.finish_fold(~Reader,~Accumulator,~Context,_)) == reader : Reader}
275      {==}