Idris2Doc : Pact.API

Pact.API

(source)
Define the API.

Reexports

importpublic Pact.API.Operator
importpublic Pact.API.Verb
importpublic Pact.API.MimeRender
importpublic Pact.API.Accept
importpublic Pact.API.HttpApiData
importpublic Pact.API.Component
importpublic Data.Vect.Quantifiers

Definitions

recordAPI : Type
Totality: total
Visibility: public export
Constructor: 
(:>) : AllFromHttpApiDatatypes=>ComponentlastTypetypesreqBody->Verb->API

Projections:
0.lastType : API->Type
.paths : ({rec:0} : API) ->Component (lastType{rec:0}) (types{rec:0}) (reqBody{rec:0})
.prf : ({rec:0} : API) ->AllFromHttpApiData (types{rec:0})
0.reqBody : API->Type
.types : ({rec:0} : API) ->Vect (typesLen{rec:0}) Type
0.typesLen : API->Nat
.verb : API->Verb
.types : ({rec:0} : API) ->Vect (typesLen{rec:0}) Type
Visibility: public export
types : ({rec:0} : API) ->Vect (typesLen{rec:0}) Type
Visibility: public export
.prf : ({rec:0} : API) ->AllFromHttpApiData (types{rec:0})
Visibility: public export
prf : ({rec:0} : API) ->AllFromHttpApiData (types{rec:0})
Visibility: public export
.paths : ({rec:0} : API) ->Component (lastType{rec:0}) (types{rec:0}) (reqBody{rec:0})
Visibility: public export
paths : ({rec:0} : API) ->Component (lastType{rec:0}) (types{rec:0}) (reqBody{rec:0})
Visibility: public export
.verb : API->Verb
Visibility: public export
verb : API->Verb
Visibility: public export
ApiReqBody : API->Type
Visibility: public export
GetHandlerType : (Type->Type) ->API->Type
  Get the type of the handler.
@m The type of the monad.
@ts The types of the path parameters.
@path The path.
@epType The type of the endpoint.

Returns the type of the handler.

Visibility: public export
GetEPFromAPI : (Type->Type) ->API->Type
  Get the type of the endpoint.
@m The type of the monad.
@ts The types of the path parameters.
@path The path.
@epType The type of the endpoint.

Returns the type of the endpoint.

Visibility: public export
GetEpResultTypeFromAPI : API->Type
  Get the type of the endpoint result.
@ts The types of the path parameters.
@path The path.
@epType The type of the endpoint.

Returns the type of the endpoint result.

Visibility: public export