def sample

stelliferous@0.0.2.0 · proofs/tensor_indexed_certificate.bend:11

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

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