LAWS.step: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/storage/LAWS.bend as LAWS
Lines 122-133 of bendtorch-core@0.1.0.0/src/storage/LAWS.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/storage/LAWS.bend&start_line=122&end_line=133

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

def step(storage: Storage.Storage, op: Op) -> Storage.Storage:
  match op:
    case Write{+i, value}:
      written(storage, i, value)
    case Read{+i}:
      kept(storage, i)
    case First{}:
      first(storage)
    case Second{}:
      second(storage)
    case Length{}:
      owner(Nat, Storage.length(storage))

Uses (9):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/LAWS.bend&name=Op
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/LAWS.bend&name=first
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/LAWS.bend&name=kept
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/LAWS.bend&name=owner
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/LAWS.bend&name=second
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/LAWS.bend&name=written
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/main.bend&name=Storage
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/main.bend&name=length