Documentation

Std.Internal.Http.Data.Method

Method #

This module provides the Method type that represents HTTP request methods. It defines all IANA-registered HTTP methods as distinct constructors, including standard methods (e.g. GET, POST, PUT, DELETE) and extension methods from WebDAV, CalDAV, and other specifications. Unrecognized method strings produce none from ofString?.

References:

inductive Std.Http.Method :

A method is a verb that describes the action to be performed.

Covers all methods in the IANA HTTP Method Registry.

Reference: https://www.iana.org/assignments/http-methods/http-methods.xhtml

acl : Method
Access control list for a resource. Source: https://www.rfc-editor.org/rfc/rfc3744#section-8.1
baselineControl : Method
Apply a label to a version-controlled resource baseline. Source: https://www.rfc-editor.org/rfc/rfc3253#section-12.6
bind : Method
Bind a resource to an additional URI path. Source: https://www.rfc-editor.org/rfc/rfc5842#section-4
checkin : Method
Check in a checked-out version-controlled resource. Source: https://www.rfc-editor.org/rfc/rfc3253#section-9.4
checkout : Method
Check out a version-controlled resource for modification. Source: https://www.rfc-editor.org/rfc/rfc3253#section-8.8
connect : Method
Establish a tunnel to a server (often for TLS). Source: https://httpwg.org/specs/rfc9110.html#section-9.3.6
copy : Method
Copy a resource to a new URI. Source: https://www.rfc-editor.org/rfc/rfc4918#section-9.8
delete : Method
Remove a resource. Source: https://httpwg.org/specs/rfc9110.html#section-9.3.5
get : Method
Retrieve a resource. Source: https://httpwg.org/specs/rfc9110.html#section-9.3.1
head : Method
Retrieve headers for a resource, without the body. Source: https://httpwg.org/specs/rfc9110.html#section-9.3.2
label : Method
Apply a label to a version history. Source: https://www.rfc-editor.org/rfc/rfc3253#section-8.2
link : Method
Create a link relationship between resources. Source: https://www.rfc-editor.org/rfc/rfc2068#section-19.6.1.2
lock : Method
Lock a resource to prevent concurrent modifications. Source: https://www.rfc-editor.org/rfc/rfc4918#section-9.10
merge : Method
Merge a version-controlled resource. Source: https://www.rfc-editor.org/rfc/rfc3253#section-11.2
mkactivity : Method
Create a new activity resource. Source: https://www.rfc-editor.org/rfc/rfc3253#section-13.5
mkcalendar : Method
Create a calendar collection. Source: https://www.rfc-editor.org/rfc/rfc4791#section-5.3.1
mkcol : Method
Create a collection resource (WebDAV directory). Source: https://www.rfc-editor.org/rfc/rfc4918#section-9.3
mkredirectref : Method
Create a redirect reference resource. Source: https://www.rfc-editor.org/rfc/rfc4437#section-6
mkworkspace : Method
Create a workspace resource. Source: https://www.rfc-editor.org/rfc/rfc3253#section-6.3
move : Method
Move a resource to a new URI. Source: https://www.rfc-editor.org/rfc/rfc4918#section-9.9
options : Method
Describe communication options for a resource. Source: https://httpwg.org/specs/rfc9110.html#section-9.3.7
orderpatch : Method
Reorder members of a collection. Source: https://www.rfc-editor.org/rfc/rfc3648#section-7
patch : Method
Apply partial modifications to a resource. Source: https://www.rfc-editor.org/rfc/rfc5789#section-2
post : Method
Submit data to be processed (e.g., form submission). Source: https://httpwg.org/specs/rfc9110.html#section-9.3.3
pri : Method
HTTP/2 connection preface (not used in application code). Source: https://www.rfc-editor.org/rfc/rfc9113#section-3.4
propfind : Method
Retrieve properties of a resource (WebDAV). Source: https://www.rfc-editor.org/rfc/rfc4918#section-9.1
proppatch : Method
Set or remove properties on a resource (WebDAV). Source: https://www.rfc-editor.org/rfc/rfc4918#section-9.2
put : Method
Replace a resource with new data. Source: https://httpwg.org/specs/rfc9110.html#section-9.3.4
query : Method
Perform a safe query with a request body. Source: https://www.ietf.org/archive/id/draft-ietf-httpbis-safe-method-w-body-14.html#section-2
rebind : Method
Rebind a resource to a new URI path. Source: https://www.rfc-editor.org/rfc/rfc5842#section-6
report : Method
Retrieve a report on a resource. Source: https://www.rfc-editor.org/rfc/rfc3253#section-3.6
search : Method
Search a resource. Source: https://www.rfc-editor.org/rfc/rfc5323#section-2
trace : Method
Perform a message loop-back test. Source: https://httpwg.org/specs/rfc9110.html#section-9.3.8
unbind : Method
Remove a URI binding from a resource. Source: https://www.rfc-editor.org/rfc/rfc5842#section-5
uncheckout : Method
Undo a previous checkout of a version-controlled resource. Source: https://www.rfc-editor.org/rfc/rfc3253#section-4.5
unlink : Method
Remove a link relationship between resources. Source: https://www.rfc-editor.org/rfc/rfc2068#section-19.6.1.3
unlock : Method
Unlock a resource. Source: https://www.rfc-editor.org/rfc/rfc4918#section-9.11
update : Method
Update a version-controlled resource. Source: https://www.rfc-editor.org/rfc/rfc3253#section-7.1
updateredirectref : Method
Update a redirect reference resource. Source: https://www.rfc-editor.org/rfc/rfc4437#section-7
versionControl : Method
Put a resource under version control. Source: https://www.rfc-editor.org/rfc/rfc3253#section-3.5

Instances For

@[implicit_reducible]

instance Std.Http.instReprMethod :

Equations

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

def Std.Http.instReprMethod.repr :

Method → Nat → Format

Equations

One or more equations did not get rendered due to their size.
Std.Http.instReprMethod.repr Std.Http.Method.acl prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Std.Http.Method.acl")).group prec✝
Std.Http.instReprMethod.repr Std.Http.Method.bind prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Std.Http.Method.bind")).group prec✝
Std.Http.instReprMethod.repr Std.Http.Method.checkin prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Std.Http.Method.checkin")).group prec✝
Std.Http.instReprMethod.repr Std.Http.Method.checkout prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Std.Http.Method.checkout")).group prec✝
Std.Http.instReprMethod.repr Std.Http.Method.connect prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Std.Http.Method.connect")).group prec✝
Std.Http.instReprMethod.repr Std.Http.Method.copy prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Std.Http.Method.copy")).group prec✝
Std.Http.instReprMethod.repr Std.Http.Method.delete prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Std.Http.Method.delete")).group prec✝
Std.Http.instReprMethod.repr Std.Http.Method.get prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Std.Http.Method.get")).group prec✝
Std.Http.instReprMethod.repr Std.Http.Method.head prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Std.Http.Method.head")).group prec✝
Std.Http.instReprMethod.repr Std.Http.Method.label prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Std.Http.Method.label")).group prec✝
Std.Http.instReprMethod.repr Std.Http.Method.link prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Std.Http.Method.link")).group prec✝
Std.Http.instReprMethod.repr Std.Http.Method.lock prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Std.Http.Method.lock")).group prec✝
Std.Http.instReprMethod.repr Std.Http.Method.merge prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Std.Http.Method.merge")).group prec✝
Std.Http.instReprMethod.repr Std.Http.Method.mkactivity prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Std.Http.Method.mkactivity")).group prec✝
Std.Http.instReprMethod.repr Std.Http.Method.mkcalendar prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Std.Http.Method.mkcalendar")).group prec✝
Std.Http.instReprMethod.repr Std.Http.Method.mkcol prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Std.Http.Method.mkcol")).group prec✝
Std.Http.instReprMethod.repr Std.Http.Method.mkworkspace prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Std.Http.Method.mkworkspace")).group prec✝
Std.Http.instReprMethod.repr Std.Http.Method.move prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Std.Http.Method.move")).group prec✝
Std.Http.instReprMethod.repr Std.Http.Method.options prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Std.Http.Method.options")).group prec✝
Std.Http.instReprMethod.repr Std.Http.Method.orderpatch prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Std.Http.Method.orderpatch")).group prec✝
Std.Http.instReprMethod.repr Std.Http.Method.patch prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Std.Http.Method.patch")).group prec✝
Std.Http.instReprMethod.repr Std.Http.Method.post prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Std.Http.Method.post")).group prec✝
Std.Http.instReprMethod.repr Std.Http.Method.pri prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Std.Http.Method.pri")).group prec✝
Std.Http.instReprMethod.repr Std.Http.Method.propfind prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Std.Http.Method.propfind")).group prec✝
Std.Http.instReprMethod.repr Std.Http.Method.proppatch prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Std.Http.Method.proppatch")).group prec✝
Std.Http.instReprMethod.repr Std.Http.Method.put prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Std.Http.Method.put")).group prec✝
Std.Http.instReprMethod.repr Std.Http.Method.query prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Std.Http.Method.query")).group prec✝
Std.Http.instReprMethod.repr Std.Http.Method.rebind prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Std.Http.Method.rebind")).group prec✝
Std.Http.instReprMethod.repr Std.Http.Method.report prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Std.Http.Method.report")).group prec✝
Std.Http.instReprMethod.repr Std.Http.Method.search prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Std.Http.Method.search")).group prec✝
Std.Http.instReprMethod.repr Std.Http.Method.trace prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Std.Http.Method.trace")).group prec✝
Std.Http.instReprMethod.repr Std.Http.Method.unbind prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Std.Http.Method.unbind")).group prec✝
Std.Http.instReprMethod.repr Std.Http.Method.uncheckout prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Std.Http.Method.uncheckout")).group prec✝
Std.Http.instReprMethod.repr Std.Http.Method.unlink prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Std.Http.Method.unlink")).group prec✝
Std.Http.instReprMethod.repr Std.Http.Method.unlock prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Std.Http.Method.unlock")).group prec✝
Std.Http.instReprMethod.repr Std.Http.Method.update prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Std.Http.Method.update")).group prec✝

Instances For

def Std.Http.instInhabitedMethod.default :

Equations

Std.Http.instInhabitedMethod.default = Std.Http.Method.acl

Instances For

@[implicit_reducible]

instance Std.Http.instInhabitedMethod :

Inhabited Method

Equations

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

@[implicit_reducible]

instance Std.Http.instBEqMethod :

Equations

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

def Std.Http.instBEqMethod.beq :

Method → Method → Bool

Equations

Std.Http.instBEqMethod.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

@[implicit_reducible]

instance Std.Http.instDecidableEqMethod :

DecidableEq Method

Equations

Std.Http.instDecidableEqMethod x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Std.Http.Method.ofString? :

String → Option Method

Converts a String into a Method. Returns none for unrecognized method strings.

Equations

Std.Http.Method.ofString? "ACL" = some Std.Http.Method.acl
Std.Http.Method.ofString? "BASELINE-CONTROL" = some Std.Http.Method.baselineControl
Std.Http.Method.ofString? "BIND" = some Std.Http.Method.bind
Std.Http.Method.ofString? "CHECKIN" = some Std.Http.Method.checkin
Std.Http.Method.ofString? "CHECKOUT" = some Std.Http.Method.checkout
Std.Http.Method.ofString? "CONNECT" = some Std.Http.Method.connect
Std.Http.Method.ofString? "COPY" = some Std.Http.Method.copy
Std.Http.Method.ofString? "DELETE" = some Std.Http.Method.delete
Std.Http.Method.ofString? "GET" = some Std.Http.Method.get
Std.Http.Method.ofString? "HEAD" = some Std.Http.Method.head
Std.Http.Method.ofString? "LABEL" = some Std.Http.Method.label
Std.Http.Method.ofString? "LINK" = some Std.Http.Method.link
Std.Http.Method.ofString? "LOCK" = some Std.Http.Method.lock
Std.Http.Method.ofString? "MERGE" = some Std.Http.Method.merge
Std.Http.Method.ofString? "MKACTIVITY" = some Std.Http.Method.mkactivity
Std.Http.Method.ofString? "MKCALENDAR" = some Std.Http.Method.mkcalendar
Std.Http.Method.ofString? "MKCOL" = some Std.Http.Method.mkcol
Std.Http.Method.ofString? "MKREDIRECTREF" = some Std.Http.Method.mkredirectref
Std.Http.Method.ofString? "MKWORKSPACE" = some Std.Http.Method.mkworkspace
Std.Http.Method.ofString? "MOVE" = some Std.Http.Method.move
Std.Http.Method.ofString? "OPTIONS" = some Std.Http.Method.options
Std.Http.Method.ofString? "ORDERPATCH" = some Std.Http.Method.orderpatch
Std.Http.Method.ofString? "PATCH" = some Std.Http.Method.patch
Std.Http.Method.ofString? "POST" = some Std.Http.Method.post
Std.Http.Method.ofString? "PRI" = some Std.Http.Method.pri
Std.Http.Method.ofString? "PROPFIND" = some Std.Http.Method.propfind
Std.Http.Method.ofString? "PROPPATCH" = some Std.Http.Method.proppatch
Std.Http.Method.ofString? "PUT" = some Std.Http.Method.put
Std.Http.Method.ofString? "QUERY" = some Std.Http.Method.query
Std.Http.Method.ofString? "REBIND" = some Std.Http.Method.rebind
Std.Http.Method.ofString? "REPORT" = some Std.Http.Method.report
Std.Http.Method.ofString? "SEARCH" = some Std.Http.Method.search
Std.Http.Method.ofString? "TRACE" = some Std.Http.Method.trace
Std.Http.Method.ofString? "UNBIND" = some Std.Http.Method.unbind
Std.Http.Method.ofString? "UNCHECKOUT" = some Std.Http.Method.uncheckout
Std.Http.Method.ofString? "UNLINK" = some Std.Http.Method.unlink
Std.Http.Method.ofString? "UNLOCK" = some Std.Http.Method.unlock
Std.Http.Method.ofString? "UPDATE" = some Std.Http.Method.update
Std.Http.Method.ofString? "UPDATEREDIRECTREF" = some Std.Http.Method.updateredirectref
Std.Http.Method.ofString? "VERSION-CONTROL" = some Std.Http.Method.versionControl
Std.Http.Method.ofString? x✝ = none

Instances For

def Std.Http.Method.ofString! (s : String) :

Converts a String into a Method, panicking if unrecognized.

Equations

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

Instances For

@[implicit_reducible]

instance Std.Http.Method.instToString :

ToString Method

Equations

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

@[implicit_reducible]

instance Std.Http.Method.instEncodeV11 :

Internal.Encode Version.v11 Method

Equations

Std.Http.Method.instEncodeV11 = { encode := fun (buffer : Std.Http.Internal.ChunkedBuffer) => buffer.writeString ∘ toString }