Idris2Doc : HTTP.Method

HTTP.Method

(source)

Definitions

dataMethod : Type
  An enumeration of HTTP request methods.

Totality: total
Visibility: public export
Constructors:
GET : Method
  Requests a representation of the specified resource.
GET requests should not contain a request body.
HEAD : Method
  Requests the metadata of a resource. This is typically sent
instead of a `GET` request, for instance to determine the
`Content-Size` of a resource.
POST : Method
  Submits some data to the specified resource, often resulting
in a change of the server state.
PUT : Method
  Creates a new resource or replaces an existing resource with
the request content. Unlike `POST`, `PUT` requests are supposed
to be idempotent.
DELETE : Method
  Asks the HTTP server to delete a specified resource.
PATCH : Method
  Applies a partial modification to a resource.

Hints:
EqMethod
OrdMethod
ShowMethod