Documentation

Std.Internal.Http.Data.Status

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) :

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

Equations

Std.Http.IsValidReasonPhrase s = (s.toList.all Std.Http.Internal.Char.reasonPhraseChar = true)

Instances For

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

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.

Equations

Instances For

structure Std.Http.CustomStatus :

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.

Instances For

@[implicit_reducible]

instance Std.Http.instReprCustomStatus :

Repr CustomStatus

Equations

Std.Http.instReprCustomStatus = { reprPrec := Std.Http.instReprCustomStatus.repr }

def Std.Http.instReprCustomStatus.repr :

CustomStatus → Nat → Format

Equations

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

Instances For

def Std.Http.instBEqCustomStatus.beq :

CustomStatus → CustomStatus → Bool

Equations

One or more equations did not get rendered due to their size.
Std.Http.instBEqCustomStatus.beq x✝¹ x✝ = false

Instances For

@[implicit_reducible]

instance Std.Http.instBEqCustomStatus :

BEq CustomStatus

Equations

Std.Http.instBEqCustomStatus = { beq := Std.Http.instBEqCustomStatus.beq }

@[implicit_reducible]

instance Std.Http.instInhabitedCustomStatus :

Inhabited CustomStatus

Equations

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

@[implicit_reducible]

instance Std.Http.instToStringCustomStatus :

ToString CustomStatus

Equations

Std.Http.instToStringCustomStatus = { toString := fun (s : Std.Http.CustomStatus) => s.phrase }

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.

Equations

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

Instances For

inductive Std.Http.Status :

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.

Instances For

def Std.Http.instReprStatus.repr :

Status → Nat → Format

Equations

One or more equations did not get rendered due to their size.
Std.Http.instReprStatus.repr Std.Http.Status.continue prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Std.Http.Status.continue")).group prec✝
Std.Http.instReprStatus.repr Std.Http.Status.processing prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Std.Http.Status.processing")).group prec✝
Std.Http.instReprStatus.repr Std.Http.Status.earlyHints prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Std.Http.Status.earlyHints")).group prec✝
Std.Http.instReprStatus.repr Std.Http.Status.ok prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Std.Http.Status.ok")).group prec✝
Std.Http.instReprStatus.repr Std.Http.Status.created prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Std.Http.Status.created")).group prec✝
Std.Http.instReprStatus.repr Std.Http.Status.accepted prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Std.Http.Status.accepted")).group prec✝
Std.Http.instReprStatus.repr Std.Http.Status.noContent prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Std.Http.Status.noContent")).group prec✝
Std.Http.instReprStatus.repr Std.Http.Status.resetContent prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Std.Http.Status.resetContent")).group prec✝
Std.Http.instReprStatus.repr Std.Http.Status.multiStatus prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Std.Http.Status.multiStatus")).group prec✝
Std.Http.instReprStatus.repr Std.Http.Status.imUsed prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Std.Http.Status.imUsed")).group prec✝
Std.Http.instReprStatus.repr Std.Http.Status.found prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Std.Http.Status.found")).group prec✝
Std.Http.instReprStatus.repr Std.Http.Status.seeOther prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Std.Http.Status.seeOther")).group prec✝
Std.Http.instReprStatus.repr Std.Http.Status.notModified prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Std.Http.Status.notModified")).group prec✝
Std.Http.instReprStatus.repr Std.Http.Status.useProxy prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Std.Http.Status.useProxy")).group prec✝
Std.Http.instReprStatus.repr Std.Http.Status.unused prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Std.Http.Status.unused")).group prec✝
Std.Http.instReprStatus.repr Std.Http.Status.badRequest prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Std.Http.Status.badRequest")).group prec✝
Std.Http.instReprStatus.repr Std.Http.Status.unauthorized prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Std.Http.Status.unauthorized")).group prec✝
Std.Http.instReprStatus.repr Std.Http.Status.forbidden prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Std.Http.Status.forbidden")).group prec✝
Std.Http.instReprStatus.repr Std.Http.Status.notFound prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Std.Http.Status.notFound")).group prec✝
Std.Http.instReprStatus.repr Std.Http.Status.conflict prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Std.Http.Status.conflict")).group prec✝
Std.Http.instReprStatus.repr Std.Http.Status.gone prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Std.Http.Status.gone")).group prec✝
Std.Http.instReprStatus.repr Std.Http.Status.uriTooLong prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Std.Http.Status.uriTooLong")).group prec✝
Std.Http.instReprStatus.repr Std.Http.Status.imATeapot prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Std.Http.Status.imATeapot")).group prec✝
Std.Http.instReprStatus.repr Std.Http.Status.locked prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Std.Http.Status.locked")).group prec✝
Std.Http.instReprStatus.repr Std.Http.Status.tooEarly prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Std.Http.Status.tooEarly")).group prec✝
Std.Http.instReprStatus.repr Std.Http.Status.badGateway prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Std.Http.Status.badGateway")).group prec✝
Std.Http.instReprStatus.repr Std.Http.Status.loopDetected prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Std.Http.Status.loopDetected")).group prec✝
Std.Http.instReprStatus.repr Std.Http.Status.notExtended prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Std.Http.Status.notExtended")).group prec✝

Instances For

@[implicit_reducible]

instance Std.Http.instReprStatus :

Equations

Std.Http.instReprStatus = { reprPrec := Std.Http.instReprStatus.repr }

@[implicit_reducible]

instance Std.Http.instInhabitedStatus :

Inhabited Status

Equations

Std.Http.instInhabitedStatus = { default := Std.Http.instInhabitedStatus.default }

def Std.Http.instInhabitedStatus.default :

Equations

Std.Http.instInhabitedStatus.default = Std.Http.Status.continue

Instances For

@[implicit_reducible]

instance Std.Http.instBEqStatus :

Equations

Std.Http.instBEqStatus = { beq := Std.Http.instBEqStatus.beq }

def Std.Http.instBEqStatus.beq :

Status → Status → Bool

Equations

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

Instances For

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.

Equations

Std.Http.Status.continue.toCode = 100
Std.Http.Status.switchingProtocols.toCode = 101
Std.Http.Status.processing.toCode = 102
Std.Http.Status.earlyHints.toCode = 103
Std.Http.Status.ok.toCode = 200
Std.Http.Status.created.toCode = 201
Std.Http.Status.accepted.toCode = 202
Std.Http.Status.nonAuthoritativeInformation.toCode = 203
Std.Http.Status.noContent.toCode = 204
Std.Http.Status.resetContent.toCode = 205
Std.Http.Status.partialContent.toCode = 206
Std.Http.Status.multiStatus.toCode = 207
Std.Http.Status.alreadyReported.toCode = 208
Std.Http.Status.imUsed.toCode = 226
Std.Http.Status.multipleChoices.toCode = 300
Std.Http.Status.movedPermanently.toCode = 301
Std.Http.Status.found.toCode = 302
Std.Http.Status.seeOther.toCode = 303
Std.Http.Status.notModified.toCode = 304
Std.Http.Status.useProxy.toCode = 305
Std.Http.Status.unused.toCode = 306
Std.Http.Status.temporaryRedirect.toCode = 307
Std.Http.Status.permanentRedirect.toCode = 308
Std.Http.Status.badRequest.toCode = 400
Std.Http.Status.unauthorized.toCode = 401
Std.Http.Status.paymentRequired.toCode = 402
Std.Http.Status.forbidden.toCode = 403
Std.Http.Status.notFound.toCode = 404
Std.Http.Status.methodNotAllowed.toCode = 405
Std.Http.Status.notAcceptable.toCode = 406
Std.Http.Status.proxyAuthenticationRequired.toCode = 407
Std.Http.Status.requestTimeout.toCode = 408
Std.Http.Status.conflict.toCode = 409
Std.Http.Status.gone.toCode = 410
Std.Http.Status.lengthRequired.toCode = 411
Std.Http.Status.preconditionFailed.toCode = 412
Std.Http.Status.payloadTooLarge.toCode = 413
Std.Http.Status.uriTooLong.toCode = 414
Std.Http.Status.unsupportedMediaType.toCode = 415
Std.Http.Status.rangeNotSatisfiable.toCode = 416
Std.Http.Status.expectationFailed.toCode = 417
Std.Http.Status.imATeapot.toCode = 418
Std.Http.Status.misdirectedRequest.toCode = 421
Std.Http.Status.unprocessableEntity.toCode = 422
Std.Http.Status.locked.toCode = 423
Std.Http.Status.failedDependency.toCode = 424
Std.Http.Status.tooEarly.toCode = 425
Std.Http.Status.upgradeRequired.toCode = 426
Std.Http.Status.preconditionRequired.toCode = 428
Std.Http.Status.tooManyRequests.toCode = 429
Std.Http.Status.requestHeaderFieldsTooLarge.toCode = 431
Std.Http.Status.unavailableForLegalReasons.toCode = 451
Std.Http.Status.internalServerError.toCode = 500
Std.Http.Status.notImplemented.toCode = 501
Std.Http.Status.badGateway.toCode = 502
Std.Http.Status.serviceUnavailable.toCode = 503
Std.Http.Status.gatewayTimeout.toCode = 504
Std.Http.Status.httpVersionNotSupported.toCode = 505
Std.Http.Status.variantAlsoNegotiates.toCode = 506
Std.Http.Status.insufficientStorage.toCode = 507
Std.Http.Status.loopDetected.toCode = 508
Std.Http.Status.notExtended.toCode = 510
Std.Http.Status.networkAuthenticationRequired.toCode = 511
(Std.Http.Status.other a).toCode = a.code

Instances For

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

Converts a UInt16 to Status.

Equations

One or more equations did not get rendered due to their size.
Std.Http.Status.ofCode reasonPhrase 100 = some Std.Http.Status.continue
Std.Http.Status.ofCode reasonPhrase 101 = some Std.Http.Status.switchingProtocols
Std.Http.Status.ofCode reasonPhrase 102 = some Std.Http.Status.processing
Std.Http.Status.ofCode reasonPhrase 103 = some Std.Http.Status.earlyHints
Std.Http.Status.ofCode reasonPhrase 200 = some Std.Http.Status.ok
Std.Http.Status.ofCode reasonPhrase 201 = some Std.Http.Status.created
Std.Http.Status.ofCode reasonPhrase 202 = some Std.Http.Status.accepted
Std.Http.Status.ofCode reasonPhrase 203 = some Std.Http.Status.nonAuthoritativeInformation
Std.Http.Status.ofCode reasonPhrase 204 = some Std.Http.Status.noContent
Std.Http.Status.ofCode reasonPhrase 205 = some Std.Http.Status.resetContent
Std.Http.Status.ofCode reasonPhrase 206 = some Std.Http.Status.partialContent
Std.Http.Status.ofCode reasonPhrase 207 = some Std.Http.Status.multiStatus
Std.Http.Status.ofCode reasonPhrase 208 = some Std.Http.Status.alreadyReported
Std.Http.Status.ofCode reasonPhrase 226 = some Std.Http.Status.imUsed
Std.Http.Status.ofCode reasonPhrase 300 = some Std.Http.Status.multipleChoices
Std.Http.Status.ofCode reasonPhrase 301 = some Std.Http.Status.movedPermanently
Std.Http.Status.ofCode reasonPhrase 302 = some Std.Http.Status.found
Std.Http.Status.ofCode reasonPhrase 303 = some Std.Http.Status.seeOther
Std.Http.Status.ofCode reasonPhrase 304 = some Std.Http.Status.notModified
Std.Http.Status.ofCode reasonPhrase 305 = some Std.Http.Status.useProxy
Std.Http.Status.ofCode reasonPhrase 306 = some Std.Http.Status.unused
Std.Http.Status.ofCode reasonPhrase 307 = some Std.Http.Status.temporaryRedirect
Std.Http.Status.ofCode reasonPhrase 308 = some Std.Http.Status.permanentRedirect
Std.Http.Status.ofCode reasonPhrase 400 = some Std.Http.Status.badRequest
Std.Http.Status.ofCode reasonPhrase 401 = some Std.Http.Status.unauthorized
Std.Http.Status.ofCode reasonPhrase 402 = some Std.Http.Status.paymentRequired
Std.Http.Status.ofCode reasonPhrase 403 = some Std.Http.Status.forbidden
Std.Http.Status.ofCode reasonPhrase 404 = some Std.Http.Status.notFound
Std.Http.Status.ofCode reasonPhrase 405 = some Std.Http.Status.methodNotAllowed
Std.Http.Status.ofCode reasonPhrase 406 = some Std.Http.Status.notAcceptable
Std.Http.Status.ofCode reasonPhrase 407 = some Std.Http.Status.proxyAuthenticationRequired
Std.Http.Status.ofCode reasonPhrase 408 = some Std.Http.Status.requestTimeout
Std.Http.Status.ofCode reasonPhrase 409 = some Std.Http.Status.conflict
Std.Http.Status.ofCode reasonPhrase 410 = some Std.Http.Status.gone
Std.Http.Status.ofCode reasonPhrase 411 = some Std.Http.Status.lengthRequired
Std.Http.Status.ofCode reasonPhrase 412 = some Std.Http.Status.preconditionFailed
Std.Http.Status.ofCode reasonPhrase 413 = some Std.Http.Status.payloadTooLarge
Std.Http.Status.ofCode reasonPhrase 414 = some Std.Http.Status.uriTooLong
Std.Http.Status.ofCode reasonPhrase 415 = some Std.Http.Status.unsupportedMediaType
Std.Http.Status.ofCode reasonPhrase 416 = some Std.Http.Status.rangeNotSatisfiable
Std.Http.Status.ofCode reasonPhrase 417 = some Std.Http.Status.expectationFailed
Std.Http.Status.ofCode reasonPhrase 418 = some Std.Http.Status.imATeapot
Std.Http.Status.ofCode reasonPhrase 421 = some Std.Http.Status.misdirectedRequest
Std.Http.Status.ofCode reasonPhrase 422 = some Std.Http.Status.unprocessableEntity
Std.Http.Status.ofCode reasonPhrase 423 = some Std.Http.Status.locked
Std.Http.Status.ofCode reasonPhrase 424 = some Std.Http.Status.failedDependency
Std.Http.Status.ofCode reasonPhrase 425 = some Std.Http.Status.tooEarly
Std.Http.Status.ofCode reasonPhrase 426 = some Std.Http.Status.upgradeRequired
Std.Http.Status.ofCode reasonPhrase 428 = some Std.Http.Status.preconditionRequired
Std.Http.Status.ofCode reasonPhrase 429 = some Std.Http.Status.tooManyRequests
Std.Http.Status.ofCode reasonPhrase 431 = some Std.Http.Status.requestHeaderFieldsTooLarge
Std.Http.Status.ofCode reasonPhrase 451 = some Std.Http.Status.unavailableForLegalReasons
Std.Http.Status.ofCode reasonPhrase 500 = some Std.Http.Status.internalServerError
Std.Http.Status.ofCode reasonPhrase 501 = some Std.Http.Status.notImplemented
Std.Http.Status.ofCode reasonPhrase 502 = some Std.Http.Status.badGateway
Std.Http.Status.ofCode reasonPhrase 503 = some Std.Http.Status.serviceUnavailable
Std.Http.Status.ofCode reasonPhrase 504 = some Std.Http.Status.gatewayTimeout
Std.Http.Status.ofCode reasonPhrase 505 = some Std.Http.Status.httpVersionNotSupported
Std.Http.Status.ofCode reasonPhrase 506 = some Std.Http.Status.variantAlsoNegotiates
Std.Http.Status.ofCode reasonPhrase 507 = some Std.Http.Status.insufficientStorage
Std.Http.Status.ofCode reasonPhrase 508 = some Std.Http.Status.loopDetected
Std.Http.Status.ofCode reasonPhrase 510 = some Std.Http.Status.notExtended
Std.Http.Status.ofCode reasonPhrase 511 = some Std.Http.Status.networkAuthenticationRequired

Instances For

@[inline]

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

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

Equations

c.isInformational = decide (100 ≤ c.toCode ∧ c.toCode < 200)

Instances For

@[inline]

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

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

Equations

c.isSuccess = decide (200 ≤ c.toCode ∧ c.toCode < 300)

Instances For

@[inline]

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

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

Equations

c.isRedirection = decide (300 ≤ c.toCode ∧ c.toCode < 400)

Instances For

@[inline]

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

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

Equations

c.isClientError = decide (400 ≤ c.toCode ∧ c.toCode < 500)

Instances For

@[inline]

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

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

Equations

c.isServerError = decide (500 ≤ c.toCode ∧ c.toCode < 600)

Instances For

@[inline]

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

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

Equations

c.isError = decide (c.isClientError = true ∨ c.isServerError = true)

Instances For

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.

Equations

Std.Http.Status.continue.reasonPhrase = "Continue"
Std.Http.Status.switchingProtocols.reasonPhrase = "Switching Protocols"
Std.Http.Status.processing.reasonPhrase = "Processing"
Std.Http.Status.earlyHints.reasonPhrase = "Early Hints"
Std.Http.Status.ok.reasonPhrase = "OK"
Std.Http.Status.created.reasonPhrase = "Created"
Std.Http.Status.accepted.reasonPhrase = "Accepted"
Std.Http.Status.nonAuthoritativeInformation.reasonPhrase = "Non-Authoritative Information"
Std.Http.Status.noContent.reasonPhrase = "No Content"
Std.Http.Status.resetContent.reasonPhrase = "Reset Content"
Std.Http.Status.partialContent.reasonPhrase = "Partial Content"
Std.Http.Status.multiStatus.reasonPhrase = "Multi-Status"
Std.Http.Status.alreadyReported.reasonPhrase = "Already Reported"
Std.Http.Status.imUsed.reasonPhrase = "IM Used"
Std.Http.Status.multipleChoices.reasonPhrase = "Multiple Choices"
Std.Http.Status.movedPermanently.reasonPhrase = "Moved Permanently"
Std.Http.Status.found.reasonPhrase = "Found"
Std.Http.Status.seeOther.reasonPhrase = "See Other"
Std.Http.Status.notModified.reasonPhrase = "Not Modified"
Std.Http.Status.useProxy.reasonPhrase = "Use Proxy"
Std.Http.Status.unused.reasonPhrase = "Unused"
Std.Http.Status.temporaryRedirect.reasonPhrase = "Temporary Redirect"
Std.Http.Status.permanentRedirect.reasonPhrase = "Permanent Redirect"
Std.Http.Status.badRequest.reasonPhrase = "Bad Request"
Std.Http.Status.unauthorized.reasonPhrase = "Unauthorized"
Std.Http.Status.paymentRequired.reasonPhrase = "Payment Required"
Std.Http.Status.forbidden.reasonPhrase = "Forbidden"
Std.Http.Status.notFound.reasonPhrase = "Not Found"
Std.Http.Status.methodNotAllowed.reasonPhrase = "Method Not Allowed"
Std.Http.Status.notAcceptable.reasonPhrase = "Not Acceptable"
Std.Http.Status.proxyAuthenticationRequired.reasonPhrase = "Proxy Authentication Required"
Std.Http.Status.requestTimeout.reasonPhrase = "Request Timeout"
Std.Http.Status.conflict.reasonPhrase = "Conflict"
Std.Http.Status.gone.reasonPhrase = "Gone"
Std.Http.Status.lengthRequired.reasonPhrase = "Length Required"
Std.Http.Status.preconditionFailed.reasonPhrase = "Precondition Failed"
Std.Http.Status.payloadTooLarge.reasonPhrase = "Payload Too Large"
Std.Http.Status.uriTooLong.reasonPhrase = "URI Too Long"
Std.Http.Status.unsupportedMediaType.reasonPhrase = "Unsupported Media Type"
Std.Http.Status.rangeNotSatisfiable.reasonPhrase = "Range Not Satisfiable"
Std.Http.Status.expectationFailed.reasonPhrase = "Expectation Failed"
Std.Http.Status.imATeapot.reasonPhrase = "I'm a teapot"
Std.Http.Status.misdirectedRequest.reasonPhrase = "Misdirected Request"
Std.Http.Status.unprocessableEntity.reasonPhrase = "Unprocessable Entity"
Std.Http.Status.locked.reasonPhrase = "Locked"
Std.Http.Status.failedDependency.reasonPhrase = "Failed Dependency"
Std.Http.Status.tooEarly.reasonPhrase = "Too Early"
Std.Http.Status.upgradeRequired.reasonPhrase = "Upgrade Required"
Std.Http.Status.preconditionRequired.reasonPhrase = "Precondition Required"
Std.Http.Status.tooManyRequests.reasonPhrase = "Too Many Requests"
Std.Http.Status.requestHeaderFieldsTooLarge.reasonPhrase = "Request Header Fields Too Large"
Std.Http.Status.unavailableForLegalReasons.reasonPhrase = "Unavailable For Legal Reasons"
Std.Http.Status.internalServerError.reasonPhrase = "Internal Server Error"
Std.Http.Status.notImplemented.reasonPhrase = "Not Implemented"
Std.Http.Status.badGateway.reasonPhrase = "Bad Gateway"
Std.Http.Status.serviceUnavailable.reasonPhrase = "Service Unavailable"
Std.Http.Status.gatewayTimeout.reasonPhrase = "Gateway Timeout"
Std.Http.Status.httpVersionNotSupported.reasonPhrase = "HTTP Version Not Supported"
Std.Http.Status.variantAlsoNegotiates.reasonPhrase = "Variant Also Negotiates"
Std.Http.Status.insufficientStorage.reasonPhrase = "Insufficient Storage"
Std.Http.Status.loopDetected.reasonPhrase = "Loop Detected"
Std.Http.Status.notExtended.reasonPhrase = "Not Extended"
Std.Http.Status.networkAuthenticationRequired.reasonPhrase = "Network Authentication Required"
(Std.Http.Status.other a).reasonPhrase = a.phrase

Instances For

@[implicit_reducible]

instance Std.Http.Status.instToString :

ToString Status

Equations

Std.Http.Status.instToString = { toString := Std.Http.Status.reasonPhrase }

@[implicit_reducible]

instance Std.Http.Status.instEncodeV11 :

Internal.Encode Version.v11 Status

Equations

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