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

import Base
import bend-kube-runtime@0.2.0.0/src/http.bend as H

# A connection that ends before any byte of a response is lost, not broken:
# only then may a request on a reused connection be retried.
law eof_before_response_is_lost:
  for t: U32
  for h: Maybe<&2, H.Head>
  for o: List<&2, U32>
  {H.Http.eof(H.Resp{H.PHead{Nil{}, t}, h, o})
    == H.Resp{H.PLost{"connection closed before a response"}, h, o} : H.Resp}

Uses (7):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Maybe
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=bend-kube-runtime@0.2.0.0/src/http.bend&name=Head
  https://jend.leeeet.dev/definition.txt?path=bend-kube-runtime@0.2.0.0/src/http.bend&name=Http.eof
  https://jend.leeeet.dev/definition.txt?path=bend-kube-runtime@0.2.0.0/src/http.bend&name=Phase
  https://jend.leeeet.dev/definition.txt?path=bend-kube-runtime@0.2.0.0/src/http.bend&name=Resp