TraversalWitness.fold_finished: def of stelliferous@0.0.2.0
Import: import stelliferous@0.0.2.0/proofs/traversal_witness.bend as TraversalWitness
Lines 268-275 of stelliferous@0.0.2.0/proofs/traversal_witness.bend: https://jend.leeeet.dev/read.txt?path=stelliferous@0.0.2.0/proofs/traversal_witness.bend&start_line=268&end_line=275

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

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

Uses (5):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/traversal_witness.bend&name=FoldEvidence
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/traversal_witness.bend&name=first
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/traversal_array.bend&name=State
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/traversal_array.bend&name=finish_fold