LAWS.last_page_watches: law of bend-kube-runtime@0.2.0.0
Import: import bend-kube-runtime@0.2.0.0/LAWS.bend as LAWS
Lines 75-85 of bend-kube-runtime@0.2.0.0/LAWS.bend: https://jend.leeeet.dev/read.txt?path=bend-kube-runtime@0.2.0.0/LAWS.bend&start_line=75&end_line=85

import Base
import bend-kube-runtime@0.2.0.0/src/json.bend as J
import bend-kube-runtime@0.2.0.0/src/core.bend as C
import bend-kube-runtime@0.2.0.0/src/watcher.bend as W

# The last page of a list (no continue token) emits its objects, closes
# the relist with InitDone, and starts watching from the list's version.
law last_page_watches:
  for c: String
  for f: U32
  for first: Bool
  for items: List<&2, J.Json>
  for rv: String
  {W.Watcher.step(W.WState{W.WList{c}, f, first}, W.IPage{C.Page{items, rv, ""}})
    == W.Step{W.WState{W.WWatch{rv}, 0, True{}},
      W.Watcher.init_out(first, W.Watcher.page_outs(items, [W.OInitDone{}])), False{}} : W.Step}

Uses (14):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=String
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=bend-kube-runtime@0.2.0.0/src/core.bend&name=Page
  https://jend.leeeet.dev/definition.txt?path=bend-kube-runtime@0.2.0.0/src/json.bend&name=Json
  https://jend.leeeet.dev/definition.txt?path=bend-kube-runtime@0.2.0.0/src/watcher.bend&name=Input
  https://jend.leeeet.dev/definition.txt?path=bend-kube-runtime@0.2.0.0/src/watcher.bend&name=Out
  https://jend.leeeet.dev/definition.txt?path=bend-kube-runtime@0.2.0.0/src/watcher.bend&name=Phase
  https://jend.leeeet.dev/definition.txt?path=bend-kube-runtime@0.2.0.0/src/watcher.bend&name=Step
  https://jend.leeeet.dev/definition.txt?path=bend-kube-runtime@0.2.0.0/src/watcher.bend&name=WState
  https://jend.leeeet.dev/definition.txt?path=bend-kube-runtime@0.2.0.0/src/watcher.bend&name=Watcher.init_out
  https://jend.leeeet.dev/definition.txt?path=bend-kube-runtime@0.2.0.0/src/watcher.bend&name=Watcher.page_outs
  https://jend.leeeet.dev/definition.txt?path=bend-kube-runtime@0.2.0.0/src/watcher.bend&name=Watcher.step