Idris2Doc : HTTP.API.Client.Interface

HTTP.API.Client.Interface

(source)
Reexports
import public HTTP.API
import public HTTP.API.Client.Request
Definitions
interface Receive : Type -> Type
  Parameters: a
Methods:
  
0 RecConstraint : a -> Type
  Auto-implicit argument required by and passed to the
  utility functions of this interface.
  
0 RecTypes : a -> List Type
  Types of values extracted from the HTTP request
  in function `fromRequest`.
  
recs : (v : a) -> TList (RecTypes v)
  `TList` representation of `RecTypes`. This is required
  to split the `RecTypes` of several endpoint descriptions and
  pass each of them to the proper description.
  
adjRequest : (v : a) -> RecConstraint v => HList (RecTypes v) -> HTTPRequest -> HTTPRequest

Implementations:
  
Receive ReqContent
  
Receive ReqHeaders
  
Receive ReqMethod
  
Receive ReqPath
  
Receive ReqEnv
  
Receive ReqQuery
0 RecConstraint : Receive a => a -> Type
  Auto-implicit argument required by and passed to the
  utility functions of this interface.

  Totality: total
  Visibility: public export
0 RecTypes : Receive a => a -> List Type
  Types of values extracted from the HTTP request
  in function `fromRequest`.

  Totality: total
  Visibility: public export
recs : {auto __con : Receive a} -> (v : a) -> TList (RecTypes v)
  `TList` representation of `RecTypes`. This is required
  to split the `RecTypes` of several endpoint descriptions and
  pass each of them to the proper description.

  Totality: total
  Visibility: public export
adjRequest : {auto __con : Receive a} -> (v : a) -> RecConstraint v => HList (RecTypes v) -> HTTPRequest -> HTTPRequest
  Totality: total
  Visibility: public export
interface GetResponse : Type -> Type
  Parameters: a
Methods:
  
0 RespEncodings : a -> List Type
  
0 RespTypes : a -> List Type

Implementations:
  
GetResponse ReqContent
  
GetResponse ReqHeaders
  
GetResponse ReqMethod
  
GetResponse ReqPath
  
GetResponse ReqQuery
0 RespEncodings : GetResponse a => a -> List Type
  Totality: total
  Visibility: public export
0 RespTypes : GetResponse a => a -> List Type
  Totality: total
  Visibility: public export
0 AllRespTypes : All GetResponse ts => HList ts -> List Type
  Totality: total
  Visibility: public export
0 AllRespEncodings : All GetResponse ts => HList ts -> List Type
  Totality: total
  Visibility: public export
0 AllRecTypes : All Receive ts => HList ts -> List Type
  Computes the list of type of values used to adjust the HTTP request
  by a single endpoint description.

  Totality: total
  Visibility: public export
0 AllRecConstraints : All Receive ts => HList ts -> List Type
  Computes the list of type of constraints used to adjust the HTTP request
  by a single endpoint description.

  Totality: total
  Visibility: public export
endpointRequest : (endpoint : HList ts) -> {auto all : All Receive ts} -> HList (AllRecConstraints endpoint) => HList (AllRecTypes endpoint) -> HTTPRequest -> HTTPRequest
  Totality: total
  Visibility: export