def last_step

stelliferous@0.0.2.0 · proofs/traversal_batch_refinement.bend:27

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

27# A loop's last step, for every state and count.
28def last_step(~State: Data,~step: State -> State,+count: Nat,+state: State) ->
29  {Loop.run(~State,~step,1n+count,state) == step(Loop.run(~State,~step,count,state)) : State}:
30  match count:
31    case 0n: {==}
32    case 1n+ +rest: last_step(~State,~step,rest,step(state))