TensorAccessCertificate.reduce: def of stelliferous@0.0.2.0
Import: import stelliferous@0.0.2.0/proofs/tensor_access_certificate.bend as TensorAccessCertificate
Lines 267-272 of stelliferous@0.0.2.0/proofs/tensor_access_certificate.bend: https://jend.leeeet.dev/read.txt?path=stelliferous@0.0.2.0/proofs/tensor_access_certificate.bend&start_line=267&end_line=272

import Base
import stelliferous@0.0.2.0/tensor_access.bend as Access
import stelliferous@0.0.2.0/tensor_view.bend as Views
import stelliferous@0.0.2.0/proofs/storage_certificate.bend as Certificate
import stelliferous@0.0.2.0/proofs/traversal_witness.bend as TraversalWitness
import stelliferous@0.0.2.0/proofs/traversal_certificate.bend as TraversalCertificate

def reduce(~Element: Data,~Accumulator: Data,~operation: Accumulator -> Element -> Accumulator,fast: Bool,count: Nat,view: Views.View,
  -storage: Array<Element>,-initial: Accumulator,certificate: Certificate.Certificate<Element,storage>) ->
  Certificate.Certificate<Element,TraversalWitness.first(~Array<Element>,~Accumulator,Access.reduce_run(~Element,~Accumulator,~operation,fast,count,view,storage,initial))>:
  Certificate.Certificate{+depth,+equation} = certificate
  TraversalCertificate.fold_operation(~Array<Element>,~Accumulator,~ReduceCall,~Certificate.family(~Element),~reduce_operation(~Element,~Accumulator,~operation),~reduced(~Element,~Accumulator,~operation),
    ReduceCall{fast,count,view},storage,initial,Certificate.Certificate{depth,equation},Certificate.Certificate{depth,equation})

Uses (12):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Array
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/storage_certificate.bend&name=Certificate
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/storage_certificate.bend&name=family
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/tensor_access_certificate.bend&name=ReduceCall
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/tensor_access_certificate.bend&name=reduce_operation
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/tensor_access_certificate.bend&name=reduced
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/traversal_certificate.bend&name=fold_operation
  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/tensor_access.bend&name=reduce_run
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/tensor_view.bend&name=View