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

Equations

• Std.Http.Response.instInhabitedHead.default = { status := default, version := default, headers := default }

@[implicit_reducible]

instance Std.Http.Response.instInhabitedHead : Inhabited Head

Equations

• Std.Http.Response.instInhabitedHead = { default := Std.Http.Response.instInhabitedHead.default }

@[implicit_reducible]

instance Std.Http.Response.instReprHead : Repr Head

Equations

• Std.Http.Response.instReprHead = { reprPrec := Std.Http.Response.instReprHead.repr }

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

Equations

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

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✝

Equations

• Std.Http.instInhabitedResponse.default = { line := default, body := default, extensions := default }

@[implicit_reducible]

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

Equations

• Std.Http.instInhabitedResponse = { default := Std.Http.instInhabitedResponse.default }

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

Equations

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

@[implicit_reducible]

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

Equations

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

def Std.Http.Response.new : Builder

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

Equations

• Std.Http.Response.new = { }

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

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

Equations

• Std.Http.Response.Builder.new = { }

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

Sets the HTTP status code for the response being built.

Equations

• builder.status status = { line := have __src := builder.line; { status := status, version := __src.version, headers := __src.headers }, extensions := builder.extensions }

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

Sets the headers for the response being built.

Equations

• builder.headers headers = { line := have __src := builder.line; { status := __src.status, version := __src.version, headers := headers }, extensions := builder.extensions }

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

Adds a single header to the response being built.

Equations

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

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.

Equations

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

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.

Equations

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

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

Inserts a typed extension value into the response being built.

Equations

• builder.extension data = { line := builder.line, extensions := builder.extensions.insert data }

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.

Equations

• builder.body body = { line := builder.line, body := body, extensions := builder.extensions }

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.

Equations

• builder.build = { line := builder.line, body := ∅, extensions := builder.extensions }

def Std.Http.Response.ok : Builder

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

Equations

• Std.Http.Response.ok = Std.Http.Response.Builder.new.status Std.Http.Status.ok

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

Creates a new HTTP Response builder with the provided status.

Equations

• Std.Http.Response.withStatus status = Std.Http.Response.Builder.new.status status

def Std.Http.Response.notFound : Builder

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

Equations

• Std.Http.Response.notFound = Std.Http.Response.Builder.new.status Std.Http.Status.notFound

def Std.Http.Response.internalServerError : Builder

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

Equations

• Std.Http.Response.internalServerError = Std.Http.Response.Builder.new.status Std.Http.Status.internalServerError

def Std.Http.Response.badRequest : Builder

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

Equations

• Std.Http.Response.badRequest = Std.Http.Response.Builder.new.status Std.Http.Status.badRequest

def Std.Http.Response.created : Builder

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

Equations

• Std.Http.Response.created = Std.Http.Response.Builder.new.status Std.Http.Status.created

def Std.Http.Response.accepted : Builder

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

Equations

• Std.Http.Response.accepted = Std.Http.Response.Builder.new.status Std.Http.Status.accepted

def Std.Http.Response.unauthorized : Builder

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

Equations

• Std.Http.Response.unauthorized = Std.Http.Response.Builder.new.status Std.Http.Status.unauthorized

def Std.Http.Response.forbidden : Builder

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

Equations

• Std.Http.Response.forbidden = Std.Http.Response.Builder.new.status Std.Http.Status.forbidden

def Std.Http.Response.conflict : Builder

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

Equations

• Std.Http.Response.conflict = Std.Http.Response.Builder.new.status Std.Http.Status.conflict

def Std.Http.Response.serviceUnavailable : Builder

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

Equations

• Std.Http.Response.serviceUnavailable = Std.Http.Response.Builder.new.status Std.Http.Status.serviceUnavailable