law replay_set

bendtorch-core@0.1.0.0 · src/storage/LAWS.bend:207

import Base
import bendtorch-core@0.1.0.0/src/storage/main.bend as Storage

207law replay_set:
208  for +n: U32
209  for +value: F32
210  for +ops: List<&2, Op>
211  for +j: U32
212  for +w: F32
213  for +fits: {U32.is_le(n, 1048576) == True{} : Bool}
214  for inside: {Nat.is_lt(U32.to_nat(j), U32.to_nat(n)) == True{} : Bool}
215  {status(replay(ops, created(n, value)), j, w) == Done{Unit{}} : Result<&2, &2, Storage.Error, Unit>}