def stepped

stelliferous@0.0.2.0 · proofs/traversal_lanes_refinement.bend:170

import Base

170# The position of the model map after k steps from start.
171def stepped(steps: Nat,start: Nat) -> U32:
172  match steps:
173    case 0n: U32.from_nat(start)
174    case 1n+rest: (stepped(rest,start) + 1 : U32)