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

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
import bend-kube-runtime@0.2.0.0/src/store.bend as S

# InitDone swaps the relisted buffer in whole: objects absent from the
# relist leave the store, and the store is ready.
law init_done_swaps:
  for objs: Map<&2, J.Json>
  for buf: Map<&2, J.Json>
  for r: Bool
  {S.Store.apply(S.Store{objs, buf, r}, W.OInitDone{})
    == S.Store{buf, Map.new(&2, J.Json), True{}} : S.Store}

Uses (7):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Map
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Map.new
  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/store.bend&name=Store
  https://jend.leeeet.dev/definition.txt?path=bend-kube-runtime@0.2.0.0/src/store.bend&name=Store.apply
  https://jend.leeeet.dev/definition.txt?path=bend-kube-runtime@0.2.0.0/src/watcher.bend&name=Out