Idris2Doc : HTTP.API.Header

HTTP.API.Header

(source)
Definitions
record HeaderPart : Type
  Totality: total
  Visibility: public export
  Constructor: 
H : String -> (0 _ : Type) -> Status -> HeaderPart

  Projections:
  
.errorStatus : HeaderPart -> Status
  
.name : HeaderPart -> String
  
0 .type : HeaderPart -> Type
.name : HeaderPart -> String
  Totality: total
  Visibility: public export
name : HeaderPart -> String
  Totality: total
  Visibility: public export
0 .type : HeaderPart -> Type
  Totality: total
  Visibility: public export
0 type : HeaderPart -> Type
  Totality: total
  Visibility: public export
.errorStatus : HeaderPart -> Status
  Totality: total
  Visibility: public export
errorStatus : HeaderPart -> Status
  Totality: total
  Visibility: public export
0 HeaderTypes : List HeaderPart -> List Type
  Computes the list of types captured by a list of header descriptions.

  Totality: total
  Visibility: public export
record ReqHeaders : Type
  Wraps a list of `HeaderPart`s to account for a full description
  of values extracted from a request's headers.

  Totality: total
  Visibility: public export
  Constructor: 
Headers : List HeaderPart -> ReqHeaders

  Projection: 
.headers : ReqHeaders -> List HeaderPart
.headers : ReqHeaders -> List HeaderPart
  Totality: total
  Visibility: public export
headers : ReqHeaders -> List HeaderPart
  Totality: total
  Visibility: public export
record OAuthToken : Type
  Totality: total
  Visibility: public export
  Constructor: 
OAT : ByteString -> OAuthToken

  Projection: 
.token : OAuthToken -> ByteString

  Hints:
  
Decode OAuthToken
  
Eq OAuthToken
  
Ord OAuthToken
  
Show OAuthToken
.token : OAuthToken -> ByteString
  Totality: total
  Visibility: public export
token : OAuthToken -> ByteString
  Totality: total
  Visibility: public export