def step

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

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

122def step(storage: Storage.Storage, op: Op) -> Storage.Storage:
123  match op:
124    case Write{+i, value}:
125      written(storage, i, value)
126    case Read{+i}:
127      kept(storage, i)
128    case First{}:
129      first(storage)
130    case Second{}:
131      second(storage)
132    case Length{}:
133      owner(Nat, Storage.length(storage))