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

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

# A relist starts from an empty buffer, whatever the store held.
law init_clears_buffer:
  for objs: Map<&2, J.Json>
  for buf: Map<&2, J.Json>
  for r: Bool
  {S.Store.apply(S.Store{objs, buf, r}, W.OInit{})
    == S.Store{objs, Map.new(&2, J.Json), r} : 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