law first_page_inits

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

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

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