
  0 | module HTTP.Method
  1 | 
  2 | import Derive.Prelude
  3 | 
  4 | %default total
  5 | %language ElabReflection
  6 | 
  7 | ||| An enumeration of HTTP request methods.
  8 | public export
  9 | data Method : Type where
 10 | 
 11 |   ||| Requests a representation of the specified resource.
 12 |   ||| GET requests should not contain a request body.
 13 |   GET    : Method
 14 | 
 15 |   ||| Requests the metadata of a resource. This is typically sent
 16 |   ||| instead of a `GET` request, for instance to determine the
 17 |   ||| `Content-Size` of a resource.
 18 |   HEAD   : Method
 19 | 
 20 |   ||| Submits some data to the specified resource, often resulting
 21 |   ||| in a change of the server state.
 22 |   POST   : Method
 23 | 
 24 |   ||| Creates a new resource or replaces an existing resource with
 25 |   ||| the request content. Unlike `POST`, `PUT` requests are supposed
 26 |   ||| to be idempotent.
 27 |   PUT    : Method
 28 | 
 29 |   ||| Asks the HTTP server to delete a specified resource.
 30 |   DELETE : Method
 31 | 
 32 |   ||| Applies a partial modification to a resource.
 33 |   PATCH : Method
 34 | 
 35 | %runElab derive "Method" [Show,Eq,Ord]
 36 |