~/jendhub

def run_indexed

stelliferous@0.0.2.0 · proofs/traversal_map_readback.bend:22

import stelliferous@0.0.2.0/proofs/traversal_map_readback.bend as TraversalMapReadback
import Base
import stelliferous@0.0.2.0/traversal_array.bend as Traversal
import stelliferous@0.0.2.0/traversal_loop.bend as Loop
import stelliferous@0.0.2.0/proofs/traversal_array_refinement.bend as ArrayLaws
import stelliferous@0.0.2.0/proofs/storage_tree_model.bend as Tree

22def run_indexed(~Element: Data,~Context: Data,~operation: Context -> U32 -> Element -> Element,count: Nat,position: U32,context: Context,input: Tree.Tree<Element>) -> Tree.Tree<Element>:
23  output(~Element,~Context,Loop.run(~Traversal.State<&2,&2,Unit,Tree.Tree<Element>,Context>,~ArrayLaws.model_map_step(~Element,~Context,~operation),
24    count,Traversal.State{Unit{},input,position,context}))

Uses (8)

Used by (9)