def map_run

stelliferous@0.0.2.0 · proofs/traversal_witness.bend:197

import Base
import stelliferous@0.0.2.0/traversal_loop.bend as Loop
import stelliferous@0.0.2.0/traversal_array.bend as Traversal

197def map_run(~Element: Data,~Context: Data,~map: Context -> Element -> Element,+depth: Nat,count: Nat,
198  -state: Traversal.State<&2,&1,Unit,Array<Element>,Context>,evidence: MapEvidence<Element,Context,depth,state>) ->
199  MapEvidence<Element,Context,depth,Loop.run(~Traversal.State<&2,&1,Unit,Array<Element>,Context>,~Traversal.map_step(~Element,~Context,~map),count,state)>:
200  match count:
201    case 0n: evidence
202    case 1n+rest:
203      map_run(~Element,~Context,~map,depth,rest,Traversal.map_step(~Element,~Context,~map,state),
204        map_step(~Element,~Context,~map,depth,state,evidence))