HTTP.API.Env

Definitions

record ReqEnv : Type

  Description of a form of "environment" variable that needs to
  be generated and available when processing a request.

Totality: total
Visibility: public export
Constructor: 

Env : (0 _ : Type) -> ReqEnv

Projection: 

0 .type : ReqEnv -> Type

0 .type : ReqEnv -> Type

Totality: total
Visibility: public export

0 type : ReqEnv -> Type

Totality: total
Visibility: public export

record ReqTime : Type

  Time, at which the request is being processed.

Totality: total
Visibility: public export
Constructor: 

RT : Clock UTC -> ReqTime

Projection: 

.time : ReqTime -> Clock UTC

.time : ReqTime -> Clock UTC

Totality: total
Visibility: public export

time : ReqTime -> Clock UTC

Totality: total
Visibility: public export