~/jendhub

def measured_iteration

stelliferous@0.0.2.0 · proofs/loop_projection.bend:61

import stelliferous@0.0.2.0/proofs/loop_projection.bend as LoopProjection
import Base

61def measured_iteration(~State: Data,~step: State -> State,~cost: State -> Nat,count: Nat,+state: State) -> Measured<State>:
62  match count:
63    case 0n: Measured{state,0n}
64    case 1n+rest:
65      add_work(State,cost(state),measured_iteration(~State,~step,~cost,rest,step(state)))

Uses (3)

Used by (1)