law watch_end_resumes

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

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

57# A watch that ends (the server's timeout) resumes from the same version,
58# with no backoff and no events.
59law watch_end_resumes:
60  for rv: String
61  for f: U32
62  for first: Bool
63  {W.Watcher.step(W.WState{W.WWatch{rv}, f, first}, W.IWatchEnd{})
64    == W.Step{W.WState{W.WWatch{rv}, 0, False{}}, Nil{}, False{}} : W.Step}

Uses (9)

Used by (0)

No other definition uses this definition.