def replay_size_empty

bendtorch-core@0.1.0.0 · src/storage/api.bend:518

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

518def replay_size_empty(+ops: List<&2, Laws.Op>) -> {Laws.size(Laws.replay(ops, Storage.Empty{})) == 0n : Nat}:
519  match ops:
520    case Nil{}:
521      {==}
522    case +op <> +later:
523      match op:
524        case Laws.Write{+i, w}:
525          replay_size_empty(later)
526        case Laws.Read{+i}:
527          replay_size_empty(later)
528        case Laws.First{}:
529          replay_size_empty(later)
530        case Laws.Second{}:
531          replay_size_empty(later)
532        case Laws.Length{}:
533          replay_size_empty(later)