Idris2Doc : HTTP.API

HTTP.API

(source)
Reexports
import public Data.Buffer
import public Data.ByteString
import public Data.List.Quantifiers
import public Data.Maybe0
import public HTTP.API.Content
import public HTTP.API.Endpoints
import public HTTP.API.Decode
import public HTTP.API.Encode
import public HTTP.API.Env
import public HTTP.API.Header
import public HTTP.API.Method
import public HTTP.API.Path
import public HTTP.API.Query
import public HTTP.API.TList
import public HTTP.Header
import public HTTP.Method
import public HTTP.RequestErr
import public HTTP.Status
import public HTTP.URI
Definitions
0 Fun : List Type -> Type -> Type
  Computes a function type from a list of argument types and a result type.
  
  This is used to compute the function type of handler of a single
  server endpoint.

  Totality: total
  Visibility: public export
0 ResultType : List Type -> Type
  Computes the result type the handler of a server endpoint.
  
  For convenience in downstream code, we only return a heterogeneous list
  in case several values are required to make adjustments to the HTTP
  response. In case of no value or a single value being required, we return
  `Unit` or the a single value, respectively.

  Totality: total
  Visibility: public export
applyHList : HList ts -> Fun ts r -> r
  Totality: total
  Visibility: export
wrapResult : TList ts -> ResultType ts -> HList ts
  converts a `ResultType` to a heterogeneous list

  Totality: total
  Visibility: export