Api.replay_size_empty: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/storage/api.bend as Api
Lines 518-533 of bendtorch-core@0.1.0.0/src/storage/api.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/storage/api.bend&start_line=518&end_line=533

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

def replay_size_empty(+ops: List<&2, Laws.Op>) -> {Laws.size(Laws.replay(ops, Storage.Empty{})) == 0n : Nat}:
  match ops:
    case Nil{}:
      {==}
    case +op <> +later:
      match op:
        case Laws.Write{+i, w}:
          replay_size_empty(later)
        case Laws.Read{+i}:
          replay_size_empty(later)
        case Laws.First{}:
          replay_size_empty(later)
        case Laws.Second{}:
          replay_size_empty(later)
        case Laws.Length{}:
          replay_size_empty(later)

Uses (6):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  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=replay
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/LAWS.bend&name=size
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/main.bend&name=Storage