Response

This module provides the Response type, which represents an HTTP response. It also defines builder functions for constructing responses and selecting common HTTP status codes.

structure Std.Http.Response.Head : Type

The main parts of a response.

• status : Status

  The HTTP status for the response.

• version : Version

  The HTTP protocol version used in the response, e.g. HTTP/1.1.

• headers : Headers

  The set of response headers, providing metadata such as Content-Type, Content-Length, and caching directives.

def Std.Http.Response.instInhabitedHead.default : Head

@[implicit_reducible]

instance Std.Http.Response.instInhabitedHead : Inhabited Head

@[implicit_reducible]

instance Std.Http.Response.instReprHead : Repr Head

def Std.Http.Response.instReprHead.repr : Head → Nat → Format

structure Std.Http.Response (t : Type) : Type

HTTP response structure parameterized by body type.

• line : Head

  The response status-line information.

• body : t

  The content of the response.

• extensions : Extensions

  Optional dynamic metadata attached to the response.

def Std.Http.instInhabitedResponse.default {a✝ : Type} [Inhabited a✝] : Response a✝

@[implicit_reducible]

instance Std.Http.instInhabitedResponse {a✝ : Type} [Inhabited a✝] : Inhabited (Response a✝)

structure Std.Http.Response.Builder : Type

Builds an HTTP Response.

• line : Head

  The response status-line information.

• extensions : Extensions

  Optional dynamic metadata attached to the response.

@[implicit_reducible]

instance Std.Http.Response.instToStringHead : ToString Head

@[implicit_reducible]

instance Std.Http.Response.instEncodeV11Head : Internal.Encode Version.v11 Head

def Std.Http.Response.new : Builder

Creates a new HTTP Response builder with default head (status: 200 OK, version: HTTP/1.1).

def Std.Http.Response.Builder.new : Builder

Creates a new HTTP Response builder with default head (status: 200 OK, version: HTTP/1.1).

def Std.Http.Response.Builder.status (builder : Builder) (status : Status) : Builder

Sets the HTTP status code for the response being built.

def Std.Http.Response.Builder.headers (builder : Builder) (headers : Headers) : Builder

Sets the headers for the response being built.

def Std.Http.Response.Builder.header (builder : Builder) (key : Header.Name) (value : Header.Value) : Builder

Adds a single header to the response being built.

def Std.Http.Response.Builder.header! (builder : Builder) (key value : String) : Builder

Adds a single header to the response being built, panics if the header is invalid.

def Std.Http.Response.Builder.header? (builder : Builder) (key value : String) : Option Builder

Adds a single header to the response being built. Returns none if the header name or value is invalid.

def Std.Http.Response.Builder.extension {α : Type u_1} (builder : Builder) [TypeName α] (data : α) : Builder

Inserts a typed extension value into the response being built.

def Std.Http.Response.Builder.body {t : Type} (builder : Builder) (body : t) : Response t

Builds and returns the final HTTP Response with the specified body.

def Std.Http.Response.Builder.build {t : Type} [EmptyCollection t] (builder : Builder) : Response t

Builds and returns the final HTTP Response with an empty body ({}). Requires an EmptyCollection instance for the response body type.

def Std.Http.Response.ok : Builder

Creates a new HTTP Response builder with the 200 status code.

def Std.Http.Response.withStatus (status : Status) : Builder

Creates a new HTTP Response builder with the provided status.

def Std.Http.Response.notFound : Builder

Creates a new HTTP Response builder with the 404 status code.

def Std.Http.Response.internalServerError : Builder

Creates a new HTTP Response builder with the 500 status code.

def Std.Http.Response.badRequest : Builder

Creates a new HTTP Response builder with the 400 status code.

def Std.Http.Response.created : Builder

Creates a new HTTP Response builder with the 201 status code.

def Std.Http.Response.accepted : Builder

Creates a new HTTP Response builder with the 202 status code.

def Std.Http.Response.unauthorized : Builder

Creates a new HTTP Response builder with the 401 status code.

def Std.Http.Response.forbidden : Builder

Creates a new HTTP Response builder with the 403 status code.

def Std.Http.Response.conflict : Builder

Creates a new HTTP Response builder with the 409 status code.

def Std.Http.Response.serviceUnavailable : Builder

Creates a new HTTP Response builder with the 503 status code.