Remove the specified headers from all responses. $$\text{stripHeaders} : \text{List HeaderName} \to \text{Middleware}$$
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
Network.Wai.Middleware.stripHeaders_nil_builder
(s : HTTP.Types.Status)
(h : HTTP.Types.ResponseHeaders)
(b : ByteArray)
:
Response.mapResponseHeaders
(fun (x : HTTP.Types.ResponseHeaders) =>
List.filter
(fun (x : HTTP.Types.Header) =>
match x with
| (n, snd) => ![].contains n)
x)
(Response.responseBuilder s h b) = Response.responseBuilder s h b
Stripping no headers preserves response headers for builder responses.
theorem
Network.Wai.Middleware.stripHeaders_nil_file
(s : HTTP.Types.Status)
(h : HTTP.Types.ResponseHeaders)
(p : String)
(fp : Option Sendfile.FilePart)
:
Response.mapResponseHeaders
(fun (x : HTTP.Types.ResponseHeaders) =>
List.filter
(fun (x : HTTP.Types.Header) =>
match x with
| (n, snd) => ![].contains n)
x)
(Response.responseFile s h p fp) = Response.responseFile s h p fp
Stripping no headers preserves response headers for file responses.
theorem
Network.Wai.Middleware.stripHeaders_nil_stream
(s : HTTP.Types.Status)
(h : HTTP.Types.ResponseHeaders)
(b : StreamingBody)
:
Response.mapResponseHeaders
(fun (x : HTTP.Types.ResponseHeaders) =>
List.filter
(fun (x : HTTP.Types.Header) =>
match x with
| (n, snd) => ![].contains n)
x)
(Response.responseStream s h b) = Response.responseStream s h b
Stripping no headers preserves response headers for stream responses.