law last_page_watches

bend-kube-runtime@0.2.0.0 · LAWS.bend:75

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

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