LAWS.first_page_inits: law of bend-kube-runtime@0.2.0.0
Import: import bend-kube-runtime@0.2.0.0/LAWS.bend as LAWS
Lines 87-91 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=87&end_line=91

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

# The first page of a relist opens it with Init.
law first_page_inits:
  for items: List<&2, J.Json>
  {W.Watcher.init_out(True{}, W.Watcher.page_outs(items, Nil{}))
    == W.OInit{} <> W.Watcher.page_outs(items, Nil{}) : List<&2, W.Out>}

Uses (6):
  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=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=Out
  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