law set_outside

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

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

184law set_outside:
185  for storage: Storage.Storage
186  for +i: U32
187  for value: F32
188  for outside: {Nat.is_lt(U32.to_nat(i), size(storage)) == False{} : Bool}
189  {status(storage, i, value) == Fail{Storage.OutOfBounds{}} : Result<&2, &2, Storage.Error, Unit>}