def Network.Wai.Middleware.addHeaders (hdrs : HTTP.Types.ResponseHeaders) : Middleware

Add the given headers to all responses. $$\text{addHeaders} : \text{ResponseHeaders} \to \text{Middleware}$$

Equations

• One or more equations did not get rendered due to their size.

theorem Network.Wai.Middleware.addHeaders_nil_builder (s : HTTP.Types.Status) (h : HTTP.Types.ResponseHeaders) (b : ByteArray) : Response.mapResponseHeaders (fun (x : HTTP.Types.ResponseHeaders) => x ++ []) (Response.responseBuilder s h b) = Response.responseBuilder s h b

Adding empty headers preserves response headers for builder responses. $$\text{mapResponseHeaders}(\cdot \mathbin{+\!\!+} []) \circ \text{responseBuilder}(s, h, b) = \text{responseBuilder}(s, h, b)$$

theorem Network.Wai.Middleware.addHeaders_nil_file (s : HTTP.Types.Status) (h : HTTP.Types.ResponseHeaders) (p : String) (fp : Option Sendfile.FilePart) : Response.mapResponseHeaders (fun (x : HTTP.Types.ResponseHeaders) => x ++ []) (Response.responseFile s h p fp) = Response.responseFile s h p fp

Adding empty headers preserves response headers for file responses.

theorem Network.Wai.Middleware.addHeaders_nil_stream (s : HTTP.Types.Status) (h : HTTP.Types.ResponseHeaders) (b : StreamingBody) : Response.mapResponseHeaders (fun (x : HTTP.Types.ResponseHeaders) => x ++ []) (Response.responseStream s h b) = Response.responseStream s h b

Adding empty headers preserves response headers for stream responses.