law get_outside

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

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

178law get_outside:
179  for storage: Storage.Storage
180  for +i: U32
181  for outside: {Nat.is_lt(U32.to_nat(i), size(storage)) == False{} : Bool}
182  {read(storage, i) == Fail{Storage.OutOfBounds{}} : Result<&2, &2, Storage.Error, F32>}