law eof_before_response_is_lost

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

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

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

Uses (7)

Used by (0)

No other definition uses this definition.