def fold_operation
stelliferous@0.0.2.0 · proofs/traversal_certificate.bend:97
import stelliferous@0.0.2.0/proofs/traversal_certificate.bend as TraversalCertificate
import Base
import stelliferous@0.0.2.0/proofs/traversal_witness.bend as TraversalWitness
97def fold_operation(~Reader: Type,~Accumulator: Data,~Metadata: Data,~ReaderCertificate: @-reader: Reader -> Data,
98 ~operation: Metadata -> Reader -> Accumulator -> Reader & Accumulator,
99 ~preserves: @metadata: Metadata -> @-reader: Reader -> @-initial: Accumulator -> ReaderCertificate(reader) ->
100 {TraversalWitness.first(~Reader,~Accumulator,operation(metadata,reader,initial)) == reader : Reader},
101 metadata: Metadata,-reader: Reader,-initial: Accumulator,proof_certificate: ReaderCertificate(reader),certificate: ReaderCertificate(reader)) ->
102 ReaderCertificate(TraversalWitness.first(~Reader,~Accumulator,operation(metadata,reader,initial))):
103 %Equal.sym(Reader,TraversalWitness.first(~Reader,~Accumulator,operation(metadata,reader,initial)),reader,
104 preserves(metadata,reader,initial,proof_certificate)) : ReaderCertificate(_)
105 certificate