TensorIndexedCertificate.sample: def of stelliferous@0.0.2.0
Import: import stelliferous@0.0.2.0/proofs/tensor_indexed_certificate.bend as TensorIndexedCertificate
Lines 11-19 of stelliferous@0.0.2.0/proofs/tensor_indexed_certificate.bend: https://jend.leeeet.dev/read.txt?path=stelliferous@0.0.2.0/proofs/tensor_indexed_certificate.bend&start_line=11&end_line=19

import Base
import stelliferous@0.0.2.0/tensor_indexed.bend as Indexed
import stelliferous@0.0.2.0/proofs/traversal_witness.bend as TraversalWitness

def sample(~Element: Data,~Context: Data,~index: Context -> U32 -> U32,~operation: U32 -> Element -> Element,
  -input: Array<Element>,+context: Context,+position: U32,-result: Array<Element> & Element,
  evidence: TraversalWitness.Sample<Array<Element>,Element,input,result>) ->
  TraversalWitness.Sample<Array<Element>,Element,input,Indexed.value(~Element,~Context,~index,~operation,context,position,result)>:
  match evidence:
    case TraversalWitness.Sample{value,equation}:
      %Equal.sym(Array<Element> & Element,result,(input,value),equation) :
        TraversalWitness.Sample<Array<Element>,Element,input,Indexed.value(~Element,~Context,~index,~operation,context,position,_)>
      TraversalWitness.Sample{operation(index(context,position),value),{==}}

Uses (7):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Array
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Pair
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Sigma
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/traversal_witness.bend&name=Sample
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/tensor_indexed.bend&name=value