Idris2Doc : HTTP.API.Method

HTTP.API.Method

(source)

Reexports

import public Data.Maybe0

Definitions

record ReqMethod : Type
  Data type describing the method (verb), response status code,
as well as encoding formats and content type (if any) of a HTTP
endpoint.

Please note that `format` and `result` refer to the format and
type of the content in the server's *response* body.

See `HTTP.API.Content` for a way to describe format and content type
in the HTTP *request* body.

Totality: total
Visibility: public export
Constructor: 
M : Method -> Status -> (0 _ : List Type) -> Maybe0 Type -> ReqMethod

Projections:
0 .formats : ReqMethod -> List Type
.method : ReqMethod -> Method
.result : ReqMethod -> Maybe0 Type
.status : ReqMethod -> Status
.method : ReqMethod -> Method
Visibility: public export
method : ReqMethod -> Method
Visibility: public export
.status : ReqMethod -> Status
Visibility: public export
status : ReqMethod -> Status
Visibility: public export
0 .formats : ReqMethod -> List Type
Visibility: public export
0 formats : ReqMethod -> List Type
Visibility: public export
.result : ReqMethod -> Maybe0 Type
Visibility: public export
result : ReqMethod -> Maybe0 Type
Visibility: public export
0 MethodResults : ReqMethod -> List Type
Visibility: public export
Get : (0 _ : List Type) -> (0 _ : Type) -> ReqMethod
Visibility: public export
Post : (0 _ : List Type) -> (0 _ : Type) -> ReqMethod
Visibility: public export
PostCreated : (0 _ : List Type) -> (0 _ : Type) -> ReqMethod
Visibility: public export
Put : (0 _ : List Type) -> (0 _ : Type) -> ReqMethod
Visibility: public export
PutCreated : (0 _ : List Type) -> (0 _ : Type) -> ReqMethod
Visibility: public export
Patch : (0 _ : List Type) -> (0 _ : Type) -> ReqMethod
Visibility: public export
Head : ReqMethod
Visibility: public export
Delete : ReqMethod
Visibility: public export
Post' : ReqMethod
Visibility: public export
Put' : ReqMethod
Visibility: public export
Patch' : ReqMethod
Visibility: public export