Status

This module defines the Status type, a representation of HTTP status codes. Status codes are three-digit integer codes that describe the result of an HTTP request. This implementation includes common named statuses and supports custom codes through Status.other.

Reference: https://httpwg.org/specs/rfc9110.html#status.codes

@[reducible, inline]

abbrev Std.Http.IsValidReasonPhrase (s : String) : Prop

A proposition stating that s is a valid HTTP reason phrase: every character passes Char.reasonPhraseChar per RFC 9110 §15.

Reference: https://httpwg.org/specs/rfc9110.html#reason.phrase

def Std.Http.isKnownStatusCode (code : UInt16) : Bool

Returns true for every status code that has a dedicated named constructor in Status. Used to ensure Status.other is never constructed with a code that already has a name.

structure Std.Http.CustomStatus : Type

A custom HTTP status with a numeric code and a reason phrase. Used to represent status codes not enumerated as dedicated constructors in Status. The code must be in the range 100–999 (a three-digit integer per RFC 9112 §4) and must not correspond to any named constructor.

Reference: https://httpwg.org/specs/rfc9110.html#status.codes

• code : UInt16

  The numeric status code.

• phrase : String

  The reason phrase associated with the status code.

• validReasonPhrase : IsValidReasonPhrase self.phrase

  Proof that the reason phrase contains only valid characters.

• validCode : 100 ≤ self.code ∧ self.code ≤ 999

  Proof that the code is a valid HTTP status code (100–999), i.e. a three-digit integer as required by RFC 9112 §4.

• validUnknown : ¬isKnownStatusCode self.code = true

  Proof that the code does not clash with any named Status constructor.

@[implicit_reducible]

instance Std.Http.instReprCustomStatus : Repr CustomStatus

def Std.Http.instReprCustomStatus.repr : CustomStatus → Nat → Format

def Std.Http.instBEqCustomStatus.beq : CustomStatus → CustomStatus → Bool

@[implicit_reducible]

instance Std.Http.instBEqCustomStatus : BEq CustomStatus

@[implicit_reducible]

instance Std.Http.instInhabitedCustomStatus : Inhabited CustomStatus

@[implicit_reducible]

instance Std.Http.instToStringCustomStatus : ToString CustomStatus

def Std.Http.CustomStatus.ofCodeAndPhrase? (code : UInt16) (phrase : String) : Option CustomStatus

Attempts to create a CustomStatus from a numeric code and a reason phrase string, returning none if the phrase contains invalid characters.

inductive Std.Http.Status : Type

HTTP Status codes. Status codes are three-digit integer codes that describe the result of an HTTP request. This implementation includes common named statuses and supports custom codes through Status.other.

Reference: https://httpwg.org/specs/rfc9110.html#status.codes

• continue : Status

  100 Continue

• switchingProtocols : Status

  101 Switching Protocols

• processing : Status

  102 Processing

• earlyHints : Status

  103 Early Hints

• ok : Status

  200 OK

• created : Status

  201 Created

• accepted : Status

  202 Accepted

• nonAuthoritativeInformation : Status

  203 Non-Authoritative Information

• noContent : Status

  204 No Content

• resetContent : Status

  205 Reset Content

• partialContent : Status

  206 Partial Content

• multiStatus : Status

  207 Multi-Status

• alreadyReported : Status

  208 Already Reported

• imUsed : Status

  226 IM Used

• multipleChoices : Status

  300 Multiple Choices

• movedPermanently : Status

  301 Moved Permanently

• found : Status

  302 Found

• seeOther : Status

  303 See Other

• notModified : Status

  304 Not Modified

• useProxy : Status

  305 Use Proxy

• unused : Status

  306 Unused

• temporaryRedirect : Status

  307 Temporary Redirect

• permanentRedirect : Status

  308 Permanent Redirect

• badRequest : Status

  400 Bad Request

• unauthorized : Status

  401 Unauthorized

• paymentRequired : Status

  402 Payment Required

• forbidden : Status

  403 Forbidden

• notFound : Status

  404 Not Found

• methodNotAllowed : Status

  405 Method Not Allowed

• notAcceptable : Status

  406 Not Acceptable

• proxyAuthenticationRequired : Status

  407 Proxy Authentication Required

• requestTimeout : Status

  408 Request Timeout

• conflict : Status

  409 Conflict

• gone : Status

  410 Gone

• lengthRequired : Status

  411 Length Required

• preconditionFailed : Status

  412 Precondition Failed

• payloadTooLarge : Status

  413 Payload Too Large

• uriTooLong : Status

  414 URI Too Long

• unsupportedMediaType : Status

  415 Unsupported Media Type

• rangeNotSatisfiable : Status

  416 Range Not Satisfiable

• expectationFailed : Status

  417 Expectation Failed

• imATeapot : Status

  418 I'm a teapot

• misdirectedRequest : Status

  421 Misdirected Request

• unprocessableEntity : Status

  422 Unprocessable Entity

• locked : Status

  423 Locked

• failedDependency : Status

  424 Failed Dependency

• tooEarly : Status

  425 Too Early

• upgradeRequired : Status

  426 Upgrade Required

• preconditionRequired : Status

  428 Precondition Required

• tooManyRequests : Status

  429 Too Many Requests

• requestHeaderFieldsTooLarge : Status

  431 Request Header Fields Too Large

• unavailableForLegalReasons : Status

  451 Unavailable For Legal Reasons

• internalServerError : Status

  500 Internal Server Error

• notImplemented : Status

  501 Not Implemented

• badGateway : Status

  502 Bad Gateway

• serviceUnavailable : Status

  503 Service Unavailable

• gatewayTimeout : Status

  504 Gateway Timeout

• httpVersionNotSupported : Status

  505 HTTP Version Not Supported

• variantAlsoNegotiates : Status

  506 Variant Also Negotiates

• insufficientStorage : Status

  507 Insufficient Storage

• loopDetected : Status

  508 Loop Detected

• notExtended : Status

  510 Not Extended

• networkAuthenticationRequired : Status

  511 Network Authentication Required

• other (status : CustomStatus) : Status

  A custom status code not covered by the standard constructors above.

def Std.Http.instReprStatus.repr : Status → Nat → Format

@[implicit_reducible]

instance Std.Http.instReprStatus : Repr Status

@[implicit_reducible]

instance Std.Http.instInhabitedStatus : Inhabited Status

def Std.Http.instInhabitedStatus.default : Status

@[implicit_reducible]

instance Std.Http.instBEqStatus : BEq Status

def Std.Http.instBEqStatus.beq : Status → Status → Bool

def Std.Http.Status.toCode : Status → UInt16

Converts a Status to a numeric code. This is useful for sending the status code in a response.

def Std.Http.Status.ofCode (reasonPhrase : Option { x : String // IsValidReasonPhrase x }) (code : UInt16) : Option Status

Converts a UInt16 to Status.

@[inline]

def Std.Http.Status.isInformational (c : Status) : Bool

Checks if the type of the status code is informational, meaning that the request was received and the process is continuing.

Reference: https://httpwg.org/specs/rfc9110.html#status.codes

@[inline]

def Std.Http.Status.isSuccess (c : Status) : Bool

Checks if the status code is a success status, meaning that the request was successfully received, understood, and accepted.

Reference: https://httpwg.org/specs/rfc9110.html#status.codes

@[inline]

def Std.Http.Status.isRedirection (c : Status) : Bool

Checks if the type of the status code is redirection, meaning that further action needs to be taken to complete the request.

Reference: https://httpwg.org/specs/rfc9110.html#status.codes

@[inline]

def Std.Http.Status.isClientError (c : Status) : Bool

Checks if the type of the status code is a client error, meaning that the request contains bad syntax or cannot be fulfilled.

Reference: https://httpwg.org/specs/rfc9110.html#status.codes

@[inline]

def Std.Http.Status.isServerError (c : Status) : Bool

Checks if the type of the status code is a server error, meaning that the server failed to fulfill an apparently valid request.

Reference: https://httpwg.org/specs/rfc9110.html#status.codes

@[inline]

def Std.Http.Status.isError (c : Status) : Bool

Checks if the status code indicates an error (either client error 4xx or server error 5xx).

Reference: https://httpwg.org/specs/rfc9110.html#status.codes

def Std.Http.Status.reasonPhrase : Status → String

Returns the standard reason phrase for an HTTP status code as defined in RFC 9110. For known status codes this returns the canonical phrase (e.g., "OK" for 200). For unknown codes (other n s), returns the caller-supplied reason phrase s.

@[implicit_reducible]

instance Std.Http.Status.instToString : ToString Status

@[implicit_reducible]

instance Std.Http.Status.instEncodeV11 : Internal.Encode Version.v11 Status