law replay_get

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

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

198law replay_get:
199  for +n: U32
200  for +value: F32
201  for +ops: List<&2, Op>
202  for +j: U32
203  for +fits: {U32.is_le(n, 1048576) == True{} : Bool}
204  for inside: {Nat.is_lt(U32.to_nat(j), U32.to_nat(n)) == True{} : Bool}
205  {read(replay(ops, created(n, value)), j) == Done{expected(ops, U32.to_nat(n), j, value)} : Result<&2, &2, Storage.Error, F32>}