def dec_run

mylsm-lsm-store@0.3.2.0 · src/Wal.bend:195

import mylsm-lsm-store@0.3.2.0/src/Wal.bend as Wal

import Base

195# Fuel-exact runner: consumes exactly len-bounded input, returns the state
196# (no extraction — callers extract). Proof-only workhorse.
197def dec_run(fuel: Nat, rest: String, st: DecState) -> DecState:
198  match fuel rest:
199    case 0n _:
200      st
201    case 1n+f SNil{}:
202      st
203    case 1n+f SCon{h, +t}:
204      dec_run(f, t, dec_step(st, h))

Uses (4)

Used by (4)